а из нее почти даром следует тот факт, что существование ортопроекций на векторное подпространство равносильно замкнутости этого подпространства.
Это неэстетично: это лишь в сепарабельном случае, в то время как теорема о проекции сепарабельности вовсе не требует.
О сепарабельности речи не было. В моем случае теорема о неравенстве Бесселя доказывается в общей постановке (там индексы
не обязаны пробегать лишь счетное множество).
Но и даже через Бесселя/Парсеваля это чересчур громоздко и уж всяко логически позднее, чем тот факт, что минимизация расстояния эквивалентна ортогональности.
Понимаю, но это все же вкусовой момент. На мой взгляд, если изменение последовательности доказательств способно привести к упрощению доказательств, то это изменение тоже имеет свою «логику». Разумеется, я не настаиваю на этой точке зрения. Дань историческому развитию, здоровый консерватизм и т.п. — это нормально, ничего против не имею.