let Bn be Subset of (RealVectSpace (Seg n)); :: thesis: ( Bn is R-orthonormal implies Bn is linearly-independent )
assume A1: Bn is R-orthonormal ; :: thesis: Bn is linearly-independent
let l be Linear_Combination of Bn; :: according to RLVECT_3:def 1 :: thesis: ( not Sum l = 0. (RealVectSpace (Seg n)) or Carrier l = {} )
assume A2: Sum l = 0. (RealVectSpace (Seg n)) ; :: thesis: Carrier l = {}
A3: ( l is Linear_Combination of RealVectSpace (Seg n) & Carrier l c= Bn ) by RLVECT_2:def 8;
assume A4: Carrier l <> {} ; :: thesis: contradiction
consider v0 being Element of Carrier l;
A5: v0 in Carrier l by A4;
then v0 in { v2 where v2 is Element of (RealVectSpace (Seg n)) : l . v2 <> 0 } by RLVECT_2:def 6;
then consider v being Element of (RealVectSpace (Seg n)) such that
A6: ( v0 = v & l . v <> 0 ) ;
reconsider xv = v as Element of REAL n by FINSEQ_2:111;
consider F being FinSequence of the carrier of (RealVectSpace (Seg n)) such that
A7: ( F is one-to-one & rng F = Carrier l & Sum l = Sum (l (#) F) ) by RLVECT_2:def 10;
A8: ( len (l (#) F) = len F & ( for i being Element of NAT st i in dom (l (#) F) holds
(l (#) F) . i = (l . (F /. i)) * (F /. i) ) ) by RLVECT_2:def 9;
consider x0 being set such that
A9: ( x0 in dom F & v0 = F . x0 ) by A4, A7, FUNCT_1:def 5;
A10: dom F = Seg (len F) by FINSEQ_1:def 3;
reconsider nx0 = x0 as Element of NAT by A9;
A11: nx0 in dom (l (#) F) by A8, A9, A10, FINSEQ_1:def 3;
A12: F . x0 = F /. x0 by A9, PARTFUN1:def 8;
A13: (Euclid_scalar n) . v,(Sum (l (#) F)) = (Euclid_scalar n) . v,((l . (F /. nx0)) * v) by A1, A3, A5, A6, A7, A9, A11, Th46
.= |(xv,((l . (F /. nx0)) * xv))| by Th45
.= (l . (F /. nx0)) * |(xv,xv)| by EUCLID_4:27
.= (l . (F /. nx0)) * (|.xv.| ^2 ) by EUCLID_2:12
.= (l . (F /. nx0)) * (1 ^2 ) by A1, A3, A5, A6, Def5
.= l . (F /. nx0) ;
F /. nx0 in rng F by A9, A12, FUNCT_1:def 5;
then F /. nx0 in { v3 where v3 is Element of (RealVectSpace (Seg n)) : l . v3 <> 0 } by A7, RLVECT_2:def 6;
then A14: ex v3 being Element of (RealVectSpace (Seg n)) st
( v3 = F /. nx0 & l . v3 <> 0 ) ;
(Euclid_scalar n) . v,(Sum (l (#) F)) = |(xv,(0* n))| by A2, A7, Th45
.= 0 by EUCLID_4:23 ;
hence contradiction by A13, A14; :: thesis: verum