theorem Th7: :: RUSUB_6:9

for H being RealUnitarySpace
for x being FinSequence of H st x is one-to-one & rng x is linearly-independent & 1 <= len x holds
ex e being FinSequence of H st
( len x = len e & rng e is OrthonormalFamily of H & e is one-to-one & Lin (rng x) = Lin (rng e) & e /. 1 = (1 / ||.(x /. 1).||) * (x /. 1) & ( for k being Nat st 1 <= k & k < len x holds
ex g being FinSequence of H st
( g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] & e /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) ) & ( for k being Nat st k <= len x holds
( rng (e | k) is OrthonormalFamily of H & e | k is one-to-one & Lin (rng (x | k)) = Lin (rng (e | k)) ) ) )