:: deftheorem Def2 defines GramSchmidt RUSUB_6:def 4 :
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
for b₃ being FinSequence of H holds
( b₃ = GramSchmidt x iff ( len x = len b₃ & rng b₃ is OrthonormalFamily of H & b₃ is one-to-one & Lin (rng x) = Lin (rng b₃) & b₃ /. 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)),(b₃ | k)] & b₃ /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) ) & ( for k being Nat st k <= len x holds
( rng (b₃ | k) is OrthonormalFamily of H & b₃ | k is one-to-one & Lin (rng (x | k)) = Lin (rng (b₃ | k)) ) ) ) );