let H be RealUnitarySpace; :: thesis: for x being FinSequence of H st x is one-to-one & rng x is linearly-independent & 1 <= len x holds
rng (GramSchmidt x) is linearly-independent
let x be FinSequence of H; :: thesis: ( x is one-to-one & rng x is linearly-independent & 1 <= len x implies rng (GramSchmidt x) is linearly-independent )
assume ( x is one-to-one & rng x is linearly-independent & 1 <= len x ) ; :: thesis: rng (GramSchmidt x) is linearly-independent
then ( len x = len (GramSchmidt x) & rng (GramSchmidt x) is OrthonormalFamily of H & GramSchmidt x is one-to-one ) by Def2;
hence rng (GramSchmidt x) is linearly-independent by Th8; :: thesis: verum