какая это тягомотина, проверять, что произведение фундаментальных последовательностей фундаментальна
Это тягомотина примерно настолько же, насколько тягомотина доказывать, что произведение сходящихся последовательностей сходится, а делать это всё равно придётся.
нужно лишь проверить, что исчезающие последовательности образуют идеал в кольце фундаментальных последовательностей. Вот и получается конструкция пополнения произвольного нормированного поля. Ну и небольшая модификация этой конструкции заодно даст поле гипервещественных чисел.
Я вот про это не знаю, но операции установить всё равно как-то могу. Например, суммой фундаментальных последовательностей

и

называется фундаментальная (пусть мы уже доказали, что она фундаментальна) последовательность

. Фундаментальные последовательности эквивалентны, если их разность сходится к нулю. Осталось доказать, что если

, то

Далее устанавливаем изоморфизм между классами фундаментальными последовательностей, сходящихся к рациональным числам и рациональными числами. И доказываем, что существует поле, являющееся расширением поля рациональных чисел, изоморфное полю классов фундаментальных последовательностей. Это расширение называем полем вещественных чисел. Если кто-нибудь хочет, напишу доказательство .