Подход ewertа. Ссылаемся на теорему "Во всяком n-мерном евклидовом пространстве существует ортонормированный базис"
Не ссылаемся: это утверждение -- формально более сильное, чем запрашивалось в стартовом посте (там ничего не говорилось про линейную независимость).
Для доказательства только существования ортогонального набора линейная независимость никак не нужна (хотя сама по себе она и святое, причём тривиально святое). Существование же сводится к утверждению: любой набор из менее чем
ортогональных элементов не является максимальным. Последнее же верно просто потому, что дополнительный к ним ортогональный элемент строится конструктивно -- как
, где
-- любой вектор, не входящий в линейную оболочку предыдущих
. После чего уже автоматически выписывается процедура Грама-Шмидта, но именно после -- именно в таком порядке.