let H be RealUnitarySpace; :: thesis: for G being OrthonormalFamily of H holds G is linearly-independent
let G be OrthonormalFamily of H; :: thesis: G is linearly-independent
for l being Linear_Combination of G st Sum l = 0. H holds
Carrier l = {}

proof

let l be Linear_Combination of G; :: thesis: ( Sum l = 0. H implies Carrier l = {} )
assume A1: Sum l = 0. H ; :: thesis: Carrier l = {}
consider F being FinSequence of H such that
A2: ( F is one-to-one & rng F = Carrier l & Sum l = Sum (l (#) F) ) by RLVECT_2:def 8;
assume A3: Carrier l <> {} ; :: thesis: contradiction
A4: Carrier l = { v where v is Element of H : l . v <> 0 } by RLVECT_2:def 4;
A5: Carrier l c= G by RLVECT_2:def 6;
consider y being object such that
A6: y in Carrier l by A3, XBOOLE_0:def 1;
consider u being Element of H such that
A7: ( y = u & l . u <> 0 ) by A4, A6;
consider n being object such that
A9: ( n in dom F & u = F . n ) by FUNCT_1:def 3, A2, A6, A7;
A10: dom F = Seg (len F) by FINSEQ_1:def 3;
reconsider n = n as Nat by A9;
A11: u = F /. n by A9, PARTFUN1:def 6;
( len (l (#) F) = len F & ( for i being Nat st i in dom (l (#) F) holds
(l (#) F) . i = (l . (F /. i)) * (F /. i) ) ) by RLVECT_2:def 7;
then A13: ( 1 <= n & n <= len (l (#) F) ) by A9, A10, FINSEQ_1:1;
A14: dom (l (#) F) = Seg (len (l (#) F)) by FINSEQ_1:def 3
.= Seg (len F) by RLVECT_2:def 7
.= dom F by FINSEQ_1:def 3 ;
then (l (#) F) . n = (l . (F /. n)) * (F /. n) by A9, RLVECT_2:def 7;
then A15: (l (#) F) /. n = (l . (F /. n)) * (F /. n) by A14, A9, PARTFUN1:def 6;
(F /. n) .|. ((l (#) F) /. n) = (l . (F /. n)) * ((F /. n) .|. (F /. n)) by BHSP_1:3, A15
.= (l . (F /. n)) * 1 by A5, A6, A7, BHSP_5:def 9, A11 ;
then A17: (F /. n) .|. ((l (#) F) /. n) <> 0 by A7, A9, PARTFUN1:def 6;
A18: for i being Nat st 1 <= i & i <= len (l (#) F) & n <> i holds
(F /. n) .|. ((l (#) F) /. i) = 0

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (l (#) F) & n <> i implies (F /. n) .|. ((l (#) F) /. i) = 0 )
assume A19: ( 1 <= i & i <= len (l (#) F) & n <> i ) ; :: thesis: (F /. n) .|. ((l (#) F) /. i) = 0
then A20a: i in Seg (len (l (#) F)) ;
A20: i in dom (l (#) F) by A19, FINSEQ_3:25;
then (l (#) F) . i = (l . (F /. i)) * (F /. i) by RLVECT_2:def 7;
then A21: (l (#) F) /. i = (l . (F /. i)) * (F /. i) by A20, PARTFUN1:def 6;
A22: i in dom F by A20a, A14, FINSEQ_1:def 3;
then F . i in rng F by FUNCT_1:def 3;
then F . i in G by A2, A5;
then A23: F /. i in G by A22, PARTFUN1:def 6;
A25: F . i <> F . n by A9, A22, A2, A19;
A27: F /. i <> F /. n by A9, A25, A22, PARTFUN1:def 6, A11;
thus (F /. n) .|. ((l (#) F) /. i) = (l . (F /. i)) * ((F /. n) .|. (F /. i)) by BHSP_1:3, A21
.= (l . (F /. i)) * 0 by A23, A5, A6, A7, A11, A27, BHSP_5:def 8, BHSP_5:def 9
.= 0 ; :: thesis: verum

end;

(F /. n) .|. (Sum (l (#) F)) = (F /. n) .|. ((l (#) F) /. n) by Th5, A13, A18;
hence contradiction by A17, BHSP_1:15, A1, A2; :: thesis: verum

end;

hence G is linearly-independent by RLVECT_3:def 1; :: thesis: verum