let H be RealUnitarySpace; :: thesis:
set CH = the carrier of H;
let x be FinSequence of H; :: thesis:
assume A1: ( x is one-to-one & rng x is linearly-independent & 1 <= len x ) ; :: thesis:
len (<*> the carrier of H) = 0 ;
then A2: ( <*> the carrier of H in 0 -tuples_on the carrier of H & 0 <= len x ) ;
0 -tuples_on the carrier of H in { (i -tuples_on the carrier of H) where i is Nat : i <= len x } ;
then reconsider FINCH = union { (i -tuples_on the carrier of H) where i is Nat : i <= len x } as non empty set by A2, TARSKI:def 4;
set F = ProjSeq H;
defpred S₁[ object , object , object ] means ex e being the carrier of H -valued FinSequence ex n being Nat st
( e = $2 & n = $1 & ( len e < len x implies ex g being the carrier of H -valued FinSequence st
( g = (ProjSeq H) . [(x /. (1 + (len e))),e] & $3 = e ^ <*((1 / ||.((x /. (1 + (len e))) - (Sum g)).||) * ((x /. (1 + (len e))) - (Sum g)))*> ) ) );
A4: for n being Nat st 1 <= n & n < len x holds
for e being Element of FINCH ex f being Element of FINCH st S₁[n,e,f]

let n be Nat; :: thesis:
assume ( 1 <= n & n < len x ) ; :: thesis:
let e be Element of FINCH; :: thesis:
consider X being set such that
A5: ( e in X & X in { (i -tuples_on the carrier of H) where i is Nat : i <= len x } ) by TARSKI:def 4;
consider i being Nat such that
A6: ( X = i -tuples_on the carrier of H & i <= len x ) by A5;
ex e0 being Element of the carrier of H * st
( e = e0 & len e0 = i ) by A5, A6;
then reconsider e1 = e as the carrier of H -valued FinSequence ;
( len e1 < len x implies ex g being the carrier of H -valued FinSequence st
( g = (ProjSeq H) . [(x /. (1 + (len e1))),e1] & ex f being Element of FINCH st f = e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*> ) )

assume A7: len e1 < len x ; :: thesis:
set Fe = (ProjSeq H) . [(x /. (1 + (len e1))),e1];
rng e1 c= the carrier of H ;
then reconsider E1 = e1 as FinSequence of the carrier of H by FINSEQ_1:def 4;
ex Fe being FinSequence of H st
( Fe = (ProjSeq H) . ((x /. (1 + (len E1))),E1) & Fe = ((x /. (1 + (len E1))) .|. E1) (*) E1 ) by Def1;
then reconsider g = (ProjSeq H) . [(x /. (1 + (len e1))),e1] as the carrier of H -valued FinSequence ;
take g ; :: thesis:
thus g = (ProjSeq H) . [(x /. (1 + (len e1))),e1] ; :: thesis:
set f = e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*>;
len (e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*>) = (len e1) + (len <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*>) by FINSEQ_1:22
.= (len e1) + 1 by FINSEQ_1:40 ;
then A8: len (e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*>) <= len x by A7, NAT_1:13;
e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*> is FinSequence of the carrier of H by FINSEQ_1:75;
then e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*> in the carrier of H * by FINSEQ_1:def 11;
then A9: e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*> in (len (e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*>)) -tuples_on the carrier of H ;
(len (e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*>)) -tuples_on the carrier of H in { (i -tuples_on the carrier of H) where i is Nat : i <= len x } by A8;
then reconsider f = e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*> as Element of FINCH by A9, TARSKI:def 4;
take f ; :: thesis:
thus f = e1 ^ <*((1 / ||.((x /. (1 + (len e1))) - (Sum g)).||) * ((x /. (1 + (len e1))) - (Sum g)))*> ; :: thesis:

end;

hence ex f being Element of FINCH st S₁[n,e,f] ; :: thesis:

end;

set E0 = <*((1 / ||.(x /. 1).||) * (x /. 1))*>;
1 -tuples_on the carrier of H in { (i -tuples_on the carrier of H) where i is Nat : i <= len x } by A1;
then reconsider E0 = <*((1 / ||.(x /. 1).||) * (x /. 1))*> as Element of FINCH by TARSKI:def 4;
consider E being FinSequence of FINCH such that
len E = len x and
A10: ( E . 1 = E0 or len x = 0 ) and
A11: for n being Nat st 1 <= n & n < len x holds
S₁[n,E . n,E . (n + 1)] from RECDEF_1:sch 4(A4);
A14: for k being Nat st k < len x holds
ex e being FinSequence of the carrier of H st
( len e = k + 1 & E . (k + 1) = e )

proof

defpred S₂[ Nat] means ( $1 < len x implies ex e being FinSequence of the carrier of H st
( len e = $1 + 1 & E . ($1 + 1) = e ) );
A15: S₂[ 0 ]

proof

assume 0 < len x ; :: thesis:
len <*((1 / ||.(x /. 1).||) * (x /. 1))*> = 0 + 1 by FINSEQ_1:40;
hence ex e being FinSequence of the carrier of H st
( len e = 0 + 1 & E . (0 + 1) = e ) by A10, A1; :: thesis:

end;

A17: for k being Nat st S₂[k] holds
S₂[k + 1]

proof

let k be Nat; :: thesis:
assume A18: S₂[k] ; :: thesis:
assume A19: k + 1 < len x ; :: thesis:
then consider e being FinSequence of the carrier of H such that
A20: ( len e = k + 1 & E . (k + 1) = e ) by A18, NAT_1:13;
ex e being the carrier of H -valued FinSequence ex n being Nat st
( e = E . (k + 1) & n = k + 1 & ( len e < len x implies ex g being the carrier of H -valued FinSequence st
( g = (ProjSeq H) . [(x /. (1 + (len e))),e] & E . ((k + 1) + 1) = e ^ <*((1 / ||.((x /. (1 + (len e))) - (Sum g)).||) * ((x /. (1 + (len e))) - (Sum g)))*> ) ) ) by A11, A19, NAT_1:11;
then consider g being the carrier of H -valued FinSequence such that
A21: ( g = (ProjSeq H) . [(x /. (1 + (len e))),e] & E . ((k + 1) + 1) = e ^ <*((1 / ||.((x /. (1 + (len e))) - (Sum g)).||) * ((x /. (1 + (len e))) - (Sum g)))*> ) by A19, A20;
take e1 = e ^ <*((1 / ||.((x /. (1 + (len e))) - (Sum g)).||) * ((x /. (1 + (len e))) - (Sum g)))*>; :: thesis:
thus len e1 = (len e) + (len <*((1 / ||.((x /. (1 + (len e))) - (Sum g)).||) * ((x /. (1 + (len e))) - (Sum g)))*>) by FINSEQ_1:22
.= (k + 1) + 1 by A20, FINSEQ_1:40 ; :: thesis:
thus E . ((k + 1) + 1) = e1 by A21; :: thesis:

end;

for k being Nat holds S₂[k] from NAT_1:sch 2(A15, A17);
hence for k being Nat st k < len x holds
ex e being FinSequence of the carrier of H st
( len e = k + 1 & E . (k + 1) = e ) ; :: thesis:

end;

A22: for k being Nat st 1 <= k & k < len x holds
ex f, g being FinSequence of the carrier of H st
( E . k = f & len f = k & g = (ProjSeq H) . [(x /. (1 + k)),f] & E . (k + 1) = f ^ <*((1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)))*> )

proof

let k be Nat; :: thesis:
assume A23: ( 1 <= k & k < len x ) ; :: thesis:
then 1 - 1 <= k - 1 by XREAL_1:9;
then k - 1 in NAT by INT_1:3;
then reconsider k1 = k - 1 as Nat ;
k1 <= k - 0 by XREAL_1:10;
then k1 < len x by A23, XXREAL_0:2;
then A24: ex e being FinSequence of the carrier of H st
( len e = k1 + 1 & E . (k1 + 1) = e ) by A14;
consider e being the carrier of H -valued FinSequence, n being Nat such that
A25: ( e = E . k & n = k & ( len e < len x implies ex g being the carrier of H -valued FinSequence st
( g = (ProjSeq H) . [(x /. (1 + (len e))),e] & E . (k + 1) = e ^ <*((1 / ||.((x /. (1 + (len e))) - (Sum g)).||) * ((x /. (1 + (len e))) - (Sum g)))*> ) ) ) by A11, A23;
consider g being the carrier of H -valued FinSequence such that
A26: ( g = (ProjSeq H) . [(x /. (1 + (len e))),e] & E . (k + 1) = e ^ <*((1 / ||.((x /. (1 + (len e))) - (Sum g)).||) * ((x /. (1 + (len e))) - (Sum g)))*> ) by A23, A24, A25;
rng g c= the carrier of H ;
then reconsider g = g as FinSequence of the carrier of H by FINSEQ_1:def 4;
rng e c= the carrier of H ;
then reconsider e = e as FinSequence of the carrier of H by FINSEQ_1:def 4;
take e ; :: thesis:
take g ; :: thesis:
thus ( E . k = e & len e = k & g = (ProjSeq H) . [(x /. (1 + k)),e] & E . (k + 1) = e ^ <*((1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)))*> ) by A24, A25, A26; :: thesis:

end;

defpred S₂[ Nat, object , object ] means ex f, g being FinSequence of the carrier of H ex ek1 being Point of H st
( E . $1 = f & len f = $1 & ek1 = $3 & g = (ProjSeq H) . [(x /. (1 + $1)),f] & E . ($1 + 1) = f ^ <*ek1*> & ek1 = (1 / ||.((x /. (1 + $1)) - (Sum g)).||) * ((x /. (1 + $1)) - (Sum g)) );
A27: for k being Nat st 1 <= k & k < len x holds
for e being Element of H ex h being Element of H st S₂[k,e,h]

proof

let k be Nat; :: thesis:
assume A28: ( 1 <= k & k < len x ) ; :: thesis:
let e be Element of H; :: thesis:
consider f, g being FinSequence of the carrier of H such that
A29: ( E . k = f & len f = k & g = (ProjSeq H) . [(x /. (1 + k)),f] & E . (k + 1) = f ^ <*((1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)))*> ) by A28, A22;
take h = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)); :: thesis:
thus S₂[k,e,h] by A29; :: thesis:

end;

set e0 = (1 / ||.(x /. 1).||) * (x /. 1);
consider e being FinSequence of H such that
A30: len e = len x and
A31: ( e . 1 = (1 / ||.(x /. 1).||) * (x /. 1) or len x = 0 ) and
A32: for n being Nat st 1 <= n & n < len x holds
S₂[n,e . n,e . (n + 1)] from RECDEF_1:sch 4(A27);
A33a: 1 in Seg (len x) by A1;
A33: 1 in dom e by A30, A1, FINSEQ_3:25;
then A34: e /. 1 = (1 / ||.(x /. 1).||) * (x /. 1) by A1, A31, PARTFUN1:def 6;
A35: for n being Nat st 1 <= n & n < len x holds
ex f, g being FinSequence of the carrier of H st
( E . n = f & len f = n & g = (ProjSeq H) . [(x /. (1 + n)),f] & E . (n + 1) = f ^ <*(e /. (n + 1))*> & e /. (n + 1) = (1 / ||.((x /. (1 + n)) - (Sum g)).||) * ((x /. (1 + n)) - (Sum g)) )

proof

let k be Nat; :: thesis:
assume A36: ( 1 <= k & k < len x ) ; :: thesis:
then consider f, g being FinSequence of the carrier of H, ek1 being Point of H such that
A37: ( E . k = f & len f = k & ek1 = e . (k + 1) & g = (ProjSeq H) . [(x /. (1 + k)),f] & E . (k + 1) = f ^ <*ek1*> & ek1 = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) by A32;
( 1 <= k + 1 & k + 1 <= len x ) by A36, NAT_1:13;
then k + 1 in dom e by A30, FINSEQ_3:25;
then e . (k + 1) = e /. (k + 1) by PARTFUN1:def 6;
hence ex f, g being FinSequence of the carrier of H st
( E . k = f & len f = k & g = (ProjSeq H) . [(x /. (1 + k)),f] & E . (k + 1) = f ^ <*(e /. (k + 1))*> & e /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) by A37; :: thesis:

end;

take e ; :: thesis:
thus len x = len e by A30; :: thesis:
A38: for n being Nat st 1 <= n & n <= len x holds
E . n = e | n

proof

defpred S₃[ Nat] means ( 1 <= $1 & $1 <= len x implies E . $1 = e | $1 );
A39: S₃[ 0 ] ;
A40: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

let k be Nat; :: thesis:
assume A41: S₃[k] ; :: thesis:
assume A42: ( 1 <= k + 1 & k + 1 <= len x ) ; :: thesis:

per cases ;

suppose A43: k = 0 ; :: thesis:

e <> {} by A30, A1;
hence E . (k + 1) = e | (k + 1) by FINSEQ_5:20, A31, A43, A1, A10; :: thesis:

end;

suppose A45a: k <> 0 ; :: thesis:

then 1 <= k by NAT_1:14;
then consider f, g being FinSequence of the carrier of H such that
A47: ( E . k = f & len f = k & g = (ProjSeq H) . [(x /. (1 + k)),f] & E . (k + 1) = f ^ <*(e /. (k + 1))*> & e /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) by A35, A42, NAT_1:13;
A48: k + 1 in dom e by A30, A42, FINSEQ_3:25;
hence E . (k + 1) = (e | k) ^ <*(e . (k + 1))*> by PARTFUN1:def 6, A47, A45a, A41, A42, NAT_1:13, NAT_1:14
.= e | (k + 1) by FINSEQ_5:10, A48 ;
:: thesis:

end;

for k being Nat holds S₃[k] from NAT_1:sch 2(A39, A40);
hence for n being Nat st 1 <= n & n <= len x holds
E . n = e | n ; :: thesis:

end;

A49: for k being Nat st 1 <= k & k < len x holds
ex g being FinSequence of the carrier 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)) )

proof

let n be Nat; :: thesis:
assume A50: ( 1 <= n & n < len x ) ; :: thesis:
then A51: E . n = e | n by A38;
consider f, g being FinSequence of the carrier of H such that
A52: ( E . n = f & len f = n & g = (ProjSeq H) . [(x /. (1 + n)),f] & E . (n + 1) = f ^ <*(e /. (n + 1))*> & e /. (n + 1) = (1 / ||.((x /. (1 + n)) - (Sum g)).||) * ((x /. (1 + n)) - (Sum g)) ) by A35, A50;
thus ex g being FinSequence of the carrier of H st
( g = (ProjSeq H) . [(x /. (1 + n)),(e | n)] & e /. (n + 1) = (1 / ||.((x /. (1 + n)) - (Sum g)).||) * ((x /. (1 + n)) - (Sum g)) ) by A51, A52; :: thesis:

end;

defpred S₃[ Nat] means ( $1 <= len x implies ( rng (e | $1) is OrthonormalFamily of H & e | $1 is one-to-one & Lin (rng (x | $1)) = Lin (rng (e | $1)) ) );
A53: S₃[ 0 ]

proof

end;

A56: for k being Nat st S₃[k] holds
S₃[k + 1]

proof

proof

let t, u be Point of H; :: thesis:
assume A64: ( t = (e | (k + 1)) . (k + 1) & u in rng (e | k) ) ; :: thesis:
Seg (k + 1) c= Seg (len x) by A58, FINSEQ_1:5;
then A65: Seg (k + 1) c= dom e by A30, FINSEQ_1:def 3;
k <> 0 by A64;
then A66: 1 <= k by NAT_1:14;
A67: k < len x by A58, NAT_1:13;
consider g being FinSequence of the carrier of H such that
A68: ( g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] & e /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) by A66, A49, A58, NAT_1:13;
set z = x /. (1 + k);
set f = e | k;
A69: k + 1 in Seg (k + 1) by FINSEQ_1:4;
A70: t = e . (k + 1) by A64, FUNCT_1:49, FINSEQ_1:4
.= e /. (k + 1) by A69, A65, PARTFUN1:def 6 ;
A71: u .|. t = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * (u .|. ((x /. (1 + k)) - (Sum g))) by A68, A70, BHSP_1:3
.= (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((u .|. (x /. (1 + k))) - (u .|. (Sum g))) by BHSP_1:12 ;
A72: len (e | k) = k by FINSEQ_1:59, A30, A67;
then A73: dom (e | k) = Seg k by FINSEQ_1:def 3;
consider i being object such that
A74: ( i in dom (e | k) & u = (e | k) . i ) by A64, FUNCT_1:def 3;
reconsider i = i as Nat by A74;
A75a: Seg k c= Seg (k + 1) by FINSEQ_1:5, NAT_1:11;
A77: u = e . i by FUNCT_1:49, A74, A73
.= e /. i by A74, A73, A75a, A65, PARTFUN1:def 6 ;
consider Fe being FinSequence of H such that
A78: ( Fe = (ProjSeq H) . ((x /. (1 + k)),(e | k)) & Fe = ((x /. (1 + k)) .|. (e | k)) (*) (e | k) ) by Def1;
W1: len Fe = len (e | k) by A78, DefR;
then A79: ( 1 <= i & i <= len Fe ) by A72, A74, A73, FINSEQ_1:1;
then A82: g /. i = Fe . i by PARTFUN1:def 6, A68, A78, FINSEQ_3:25
.= ((x /. (1 + k)) .|. ((e | k) /. i)) * ((e | k) /. i) by A78, A79, W1, Added ;
(e | k) . i in rng (e | k) by A74, FUNCT_1:def 3;
then A83: (e | k) /. i in rng (e | k) by A74, PARTFUN1:def 6;
A84: ( 1 <= i & i <= len g ) by A68, A78, A72, A74, A73, FINSEQ_1:1, W1;
A85: u = (e | k) /. i by A74, PARTFUN1:def 6;
for n being Nat st 1 <= n & n <= len g & n <> i holds
u .|. (g /. n) = 0

proof

let n be Nat; :: thesis:
assume A86: ( 1 <= n & n <= len g & n <> i ) ; :: thesis:
then n in Seg (len Fe) by A68, A78;
then A88: n in dom Fe by FINSEQ_1:def 3;
A89: g /. n = Fe . n by A88, PARTFUN1:def 6, A68, A78
.= ((x /. (1 + k)) .|. ((e | k) /. n)) * ((e | k) /. n) by A78, A68, A86, W1, Added ;
A90: (e | k) /. i in rng (e | k) by A85, A74, FUNCT_1:def 3;
n in Seg (len (e | k)) by A86, A78, A68, W1;
then A91: n in dom (e | k) by FINSEQ_1:def 3;
then A92: (e | k) /. n = (e | k) . n by PARTFUN1:def 6;
then A93: (e | k) /. n in rng (e | k) by A91, FUNCT_1:def 3;
A94: (e | k) /. n <> (e | k) /. i by A92, A60, A86, A91, A74, PARTFUN1:def 6;
thus u .|. (g /. n) = ((e | k) /. i) .|. (((x /. (1 + k)) .|. ((e | k) /. n)) * ((e | k) /. n)) by A89, A74, PARTFUN1:def 6
.= ((x /. (1 + k)) .|. ((e | k) /. n)) * (((e | k) /. i) .|. ((e | k) /. n)) by BHSP_1:3
.= ((x /. (1 + k)) .|. ((e | k) /. n)) * 0 by BHSP_5:def 8, A94, A90, A93, A57, A58, NAT_1:13, BHSP_5:def 9
.= 0 ; :: thesis:

end;

then A95: u .|. (Sum g) = u .|. (g /. i) by A84, Th5
.= ((e | k) /. i) .|. (g /. i) by A74, PARTFUN1:def 6
.= ((x /. (1 + k)) .|. ((e | k) /. i)) * (((e | k) /. i) .|. ((e | k) /. i)) by BHSP_1:3, A82
.= ((x /. (1 + k)) .|. ((e | k) /. i)) * 1 by A83, BHSP_5:def 9, A57, A58, NAT_1:13
.= (x /. (1 + k)) .|. ((e | k) /. i) ;
(e | k) /. i = (e | k) . i by A74, PARTFUN1:def 6
.= e . i by A73, A74, FUNCT_1:49
.= e /. i by A74, A73, A75a, PARTFUN1:def 6, A65 ;
hence ( t .|. u = 0 & u .|. t = 0 ) by A71, A77, A95; :: thesis:

end;

A96: for t, u being Point of H st t in rng (e | (k + 1)) & u in rng (e | (k + 1)) & t <> u holds
t .|. u = 0

proof

let t, u be Point of H; :: thesis:
assume A97: ( t in rng (e | (k + 1)) & u in rng (e | (k + 1)) & t <> u ) ; :: thesis:
then consider nt being object such that
A98: ( nt in dom (e | (k + 1)) & t = (e | (k + 1)) . nt ) by FUNCT_1:def 3;
consider nu being object such that
A99: ( nu in dom (e | (k + 1)) & u = (e | (k + 1)) . nu ) by A97, FUNCT_1:def 3;
Seg (k + 1) c= Seg (len x) by A58, FINSEQ_1:5;
then A100: Seg (k + 1) c= dom e by A30, FINSEQ_1:def 3;
len (e | (k + 1)) = k + 1 by FINSEQ_1:59, A58, A30;
then A101: dom (e | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
reconsider nt = nt, nu = nu as Nat by A98, A99;
A102: ( 1 <= nt & nt <= k + 1 ) by A98, A101, FINSEQ_1:1;
A103: ( 1 <= nu & nu <= k + 1 ) by A99, A101, FINSEQ_1:1;

per cases ;

suppose ( nt = k + 1 or nu = k + 1 ) ; :: thesis:

then ( ( nt = k + 1 & nu < k + 1 ) or ( nt < k + 1 & nu = k + 1 ) ) by A102, A103, XXREAL_0:1, A97, A98, A99;
then ( ( nt = k + 1 & nu <= k ) or ( nt <= k & nu = k + 1 ) ) by NAT_1:13;
then A105: ( ( nt = k + 1 & nu in Seg k ) or ( nt in Seg k & nu = k + 1 ) ) by A102, A103;
( t = e . nt & u = e . nu ) by FUNCT_1:47, A98, A99;
then ( ( nt = k + 1 & u in rng (e | k) ) or ( t in rng (e | k) & nu = k + 1 ) ) by FUNCT_1:50, A105, A98, A99, A100, A101;
hence t .|. u = 0 by A63, A98, A99; :: thesis:

end;

suppose ( nt <> k + 1 & nu <> k + 1 ) ; :: thesis:

then ( nt < k + 1 & nu < k + 1 ) by A102, A103, XXREAL_0:1;
then ( nt <= k & nu <= k ) by NAT_1:13;
then A106: ( nt in Seg k & nu in Seg k ) by A102, A103;
( t = e . nt & u = e . nu ) by FUNCT_1:47, A98, A99;
then ( t in rng (e | k) & u in rng (e | k) ) by FUNCT_1:50, A106, A98, A99, A100, A101;
hence t .|. u = 0 by A97, BHSP_5:def 8, BHSP_5:def 9, A57, A58, NAT_1:13; :: thesis:

end;

A108: ||.(x /. 1).|| <> 0

proof

A109: 1 in dom x by A1, FINSEQ_3:25;
set a = ||.(x /. 1).||;
assume ||.(x /. 1).|| = 0 ; :: thesis:
then x /. 1 = 0. H by BHSP_1:26;
then x . 1 = 0. H by A1, PARTFUN1:def 6, FINSEQ_3:25;
then 0. H in rng x by A109, FUNCT_1:def 3;
hence contradiction by A1, RLVECT_3:6; :: thesis:

end;

A110: ( k <> 0 implies for g being FinSequence of the carrier of H st g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] holds
Sum g in Lin (rng (e | k)) )

proof

assume k <> 0 ; :: thesis:
let g be FinSequence of the carrier of H; :: thesis:
assume A112: g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] ; :: thesis:
set a = ||.((x /. (1 + k)) - (Sum g)).||;
set z = (x /. (1 + k)) - (Sum g);
consider Fe being FinSequence of H such that
A114: ( Fe = (ProjSeq H) . ((x /. (1 + k)),(e | k)) & Fe = ((x /. (1 + k)) .|. (e | k)) (*) (e | k) ) by Def1;
defpred S₄[ object , object ] means $2 = (x /. (1 + k)) .|. ((e | k) /. $1);
A116: for n being Nat st n in Seg (len (e | k)) holds
ex z being Element of REAL st S₄[n,z] ;
consider r being FinSequence of REAL such that
A117: ( dom r = Seg (len (e | k)) & ( for n being Nat st n in Seg (len (e | k)) holds
S₄[n,r . n] ) ) from FINSEQ_1:sch 5(A116);
A118: len r = len (e | k) by A117, FINSEQ_1:def 3;
WW: len Fe = len (e | k) by A114, DefR;
A119: for i being Nat st 1 <= i & i <= len (e | k) holds
r /. i = (x /. (1 + k)) .|. ((e | k) /. i)

proof

end;

for i being Nat st 1 <= i & i <= len (e | k) holds
Fe . i = (r /. i) * ((e | k) /. i)

proof

end;

then Fe = r (*) (e | k) by DefR, WW;
hence Sum g in Lin (rng (e | k)) by Th1, A114, A112, A118; :: thesis:

end;

A123: ( k <> 0 implies for g being FinSequence of the carrier of H st g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] holds
||.((x /. (1 + k)) - (Sum g)).|| <> 0 )

proof

assume A124: k <> 0 ; :: thesis:
let g be FinSequence of the carrier of H; :: thesis:
assume A125: g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] ; :: thesis:
set a = ||.((x /. (1 + k)) - (Sum g)).||;
set z = (x /. (1 + k)) - (Sum g);
assume ||.((x /. (1 + k)) - (Sum g)).|| = 0 ; :: thesis:
then ((x /. (1 + k)) - (Sum g)) + (Sum g) = (0. H) + (Sum g) by BHSP_1:26;
then A126: x /. (1 + k) = Sum g by RLVECT_4:1;
Seg (k + 1) c= Seg (len x) by A58, FINSEQ_1:5;
then A127: Seg (k + 1) c= dom x by FINSEQ_1:def 3;
k + 1 in dom x by A127, FINSEQ_1:4;
then x . (1 + k) = Sum g by PARTFUN1:def 6, A126;
then A129: x . (1 + k) in Lin (rng (x | k)) by A125, A110, A124, A57, A58, NAT_1:13;
A145a: for y being object holds
( y in rng (x | k) iff y in (rng (x | (k + 1))) \ {(x . (k + 1))} )

proof

let y be object ; :: thesis:

hereby :: thesis:

assume y in rng (x | k) ; :: thesis:
then consider t being object such that
A130: ( t in dom (x | k) & y = (x | k) . t ) by FUNCT_1:def 3;
A131: ( t in dom x & t in Seg k ) by RELAT_1:57, A130;
then A132: y = x . t by A130, FUNCT_1:49;
reconsider t = t as Nat by A130;
A133: ( 1 <= t & t <= k ) by A131, FINSEQ_1:1;
k < k + 1 by NAT_1:19;
then Seg k c= Seg (k + 1) by FINSEQ_1:5;
then A135: t in Seg (k + 1) by RELAT_1:57, A130;
then A136: y = (x | (k + 1)) . t by FUNCT_1:49, A132;
len (x | (k + 1)) = k + 1 by FINSEQ_1:59, A58;
then dom (x | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
then A137: y in rng (x | (k + 1)) by A136, A135, FUNCT_1:def 3;
Seg (k + 1) c= Seg (len x) by A58, FINSEQ_1:5;
then Seg (k + 1) c= dom x by FINSEQ_1:def 3;
then A139: k + 1 in dom x by FINSEQ_1:4;
t <> k + 1 by A133, NAT_1:19;
then x . t <> x . (k + 1) by A131, A139, A1;
then not y in {(x . (k + 1))} by A132, TARSKI:def 1;
hence y in (rng (x | (k + 1))) \ {(x . (k + 1))} by A137, XBOOLE_0:def 5; :: thesis:

end;

assume y in (rng (x | (k + 1))) \ {(x . (k + 1))} ; :: thesis:
then A140: ( y in rng (x | (k + 1)) & not y in {(x . (k + 1))} ) by XBOOLE_0:def 5;
then consider t being object such that
A141: ( t in dom (x | (k + 1)) & y = (x | (k + 1)) . t ) by FUNCT_1:def 3;
A142: k < k + 1 by NAT_1:19;
len (x | (k + 1)) = k + 1 by FINSEQ_1:59, A58;
then A143: dom (x | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
then A144: y = x . t by A141, FUNCT_1:49;
reconsider t = t as Nat by A141;
A145: t <> k + 1 by TARSKI:def 1, A144, A140;
M1: ( 1 <= t & t <= k + 1 ) by A141, A143, FINSEQ_1:1;
then t < k + 1 by A145, XXREAL_0:1;
then t <= k by NAT_1:13;
then A146: t in Seg k by M1;
len (x | k) = k by FINSEQ_1:59, A142, A58, XXREAL_0:2;
then A147: dom (x | k) = Seg k by FINSEQ_1:def 3;
y = (x | k) . t by A144, A146, FUNCT_1:49;
hence y in rng (x | k) by A146, A147, FUNCT_1:def 3; :: thesis:

end;

A149: rng (x | (k + 1)) is linearly-independent by RLVECT_3:5, A1, RELAT_1:70;
len (x | (k + 1)) = k + 1 by FINSEQ_1:59, A58;
then A150: dom (x | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
A151: k + 1 in Seg (k + 1) by FINSEQ_1:4;
x . (1 + k) = (x | (1 + k)) . (1 + k) by FINSEQ_1:4, FUNCT_1:49;
then x . (1 + k) in rng (x | (k + 1)) by A150, A151, FUNCT_1:def 3;
hence contradiction by RLVECT_5:17, A145a, TARSKI:2, A129, A149; :: thesis:

end;

for t being Point of H st t in rng (e | (k + 1)) holds
t .|. t = 1

proof

let t be Point of H; :: thesis:
assume A152: t in rng (e | (k + 1)) ; :: thesis:
Seg (k + 1) c= Seg (len x) by A58, FINSEQ_1:5;
then A153: Seg (k + 1) c= dom e by A30, FINSEQ_1:def 3;
len (e | (k + 1)) = k + 1 by FINSEQ_1:59, A58, A30;
then A154: dom (e | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
consider nt being object such that
A155: ( nt in dom (e | (k + 1)) & t = (e | (k + 1)) . nt ) by FUNCT_1:def 3, A152;
reconsider nt = nt as Nat by A155;
A156: t = e . nt by FUNCT_1:47, A155
.= e /. nt by A155, A154, A153, PARTFUN1:def 6 ;
A157: ( 1 <= nt & nt <= k + 1 ) by A155, A154, FINSEQ_1:1;

per cases ;

suppose A159: nt = k + 1 ; :: thesis:

per cases ;

suppose k = 0 ; :: thesis:

then A161: t = (1 / ||.(x /. 1).||) * (x /. 1) by A33, A1, A31, PARTFUN1:def 6, A156, A159;
set a = ||.(x /. 1).||;
set z = x /. 1;
A162: 1 in dom x by A1, FINSEQ_3:25;
A163: ||.(x /. 1).|| <> 0

proof

assume ||.(x /. 1).|| = 0 ; :: thesis:
then x /. 1 = 0. H by BHSP_1:26;
then x . 1 = 0. H by A1, FINSEQ_3:25, PARTFUN1:def 6;
then 0. H in rng x by A162, FUNCT_1:def 3;
hence contradiction by A1, RLVECT_3:6; :: thesis:

end;

thus t .|. t = (1 / ||.(x /. 1).||) * ((x /. 1) .|. ((1 / ||.(x /. 1).||) * (x /. 1))) by BHSP_1:def 2, A161
.= (1 / ||.(x /. 1).||) * ((1 / ||.(x /. 1).||) * ((x /. 1) .|. (x /. 1))) by BHSP_1:3
.= (1 / ||.(x /. 1).||) * ((1 / ||.(x /. 1).||) * (||.(x /. 1).|| ^2)) by Lm1
.= (1 / ||.(x /. 1).||) * ((1 / ||.(x /. 1).||) * (||.(x /. 1).|| * ||.(x /. 1).||)) by SQUARE_1:def 1
.= (1 / ||.(x /. 1).||) * (((1 / ||.(x /. 1).||) * ||.(x /. 1).||) * ||.(x /. 1).||)
.= (1 / ||.(x /. 1).||) * (1 * ||.(x /. 1).||) by A163, XCMPLX_1:87
.= 1 by A163, XCMPLX_1:87 ; :: thesis:

end;

suppose A164: k <> 0 ; :: thesis:

A166: k < len x by A58, NAT_1:13;
consider g being FinSequence of the carrier of H such that
A167: ( g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] & e /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) by A49, A164, A166, NAT_1:14;
set a = ||.((x /. (1 + k)) - (Sum g)).||;
set z = (x /. (1 + k)) - (Sum g);
thus t .|. t = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * (((x /. (1 + k)) - (Sum g)) .|. ((1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)))) by BHSP_1:def 2, A156, A167, A159
.= (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((1 / ||.((x /. (1 + k)) - (Sum g)).||) * (((x /. (1 + k)) - (Sum g)) .|. ((x /. (1 + k)) - (Sum g)))) by BHSP_1:3
.= (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((1 / ||.((x /. (1 + k)) - (Sum g)).||) * (||.((x /. (1 + k)) - (Sum g)).|| ^2)) by Lm1
.= (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((1 / ||.((x /. (1 + k)) - (Sum g)).||) * (||.((x /. (1 + k)) - (Sum g)).|| * ||.((x /. (1 + k)) - (Sum g)).||)) by SQUARE_1:def 1
.= (1 / ||.((x /. (1 + k)) - (Sum g)).||) * (((1 / ||.((x /. (1 + k)) - (Sum g)).||) * ||.((x /. (1 + k)) - (Sum g)).||) * ||.((x /. (1 + k)) - (Sum g)).||)
.= (1 / ||.((x /. (1 + k)) - (Sum g)).||) * (1 * ||.((x /. (1 + k)) - (Sum g)).||) by A123, A167, A164, XCMPLX_1:87
.= 1 by A123, A167, A164, XCMPLX_1:87 ; :: thesis:

end;

suppose nt <> k + 1 ; :: thesis:

then nt < k + 1 by A157, XXREAL_0:1;
then nt <= k by NAT_1:13;
then A169: nt in Seg k by A157;
t = e . nt by FUNCT_1:47, A155;
hence t .|. t = 1 by FUNCT_1:50, A155, A153, A154, A169, BHSP_5:def 9, NAT_1:13, A57, A58; :: thesis:

end;

hence rng (e | (k + 1)) is OrthonormalFamily of H by BHSP_5:def 8, A96, BHSP_5:def 9; :: thesis:
thus e | (k + 1) is one-to-one :: thesis:

proof

assume not e | (k + 1) is one-to-one ; :: thesis:
then consider t1, t2 being object such that
A170: ( t1 in dom (e | (k + 1)) & t2 in dom (e | (k + 1)) & (e | (k + 1)) . t1 = (e | (k + 1)) . t2 & t1 <> t2 ) ;
A171: ( t1 in dom e & t1 in Seg (k + 1) ) by A170, RELAT_1:57;
reconsider t1 = t1 as Nat by A170;
A172: ( t2 in dom e & t2 in Seg (k + 1) ) by A170, RELAT_1:57;
reconsider t2 = t2 as Nat by A170;
A173: ( not t1 in Seg k or not t2 in Seg k )

proof

assume A174: ( t1 in Seg k & t2 in Seg k ) ; :: thesis:
then A175: ( t1 in dom (e | k) & t2 in dom (e | k) ) by A171, A172, RELAT_1:57;
A176: (e | k) . t1 = e . t1 by FUNCT_1:49, A174
.= (e | (k + 1)) . t1 by FUNCT_1:49, A171 ;
(e | k) . t2 = e . t2 by FUNCT_1:49, A174
.= (e | (k + 1)) . t2 by FUNCT_1:49, A172 ;
hence contradiction by A170, A175, A60, A176; :: thesis:

end;

A179: ( 1 <= t1 & t1 <= k + 1 ) by A171, FINSEQ_1:1;
A180: ( 1 <= t2 & t2 <= k + 1 ) by A172, FINSEQ_1:1;
then ( t1 > k or t2 > k ) by A179, A173;
then ( k + 1 <= t1 or k + 1 <= t2 ) by NAT_1:13;
then ( ( 1 <= t1 & t1 <= k + 1 & t1 <> k + 1 & t2 = k + 1 ) or ( t1 = k + 1 & 1 <= t2 & t2 <= k + 1 & t2 <> k + 1 ) ) by A170, A179, A180, XXREAL_0:1;
then ( ( 1 <= t1 & t1 < k + 1 & t2 = k + 1 ) or ( t1 = k + 1 & 1 <= t2 & t2 < k + 1 ) ) by XXREAL_0:1;
then A181a: ( ( 1 <= t1 & t1 <= k & t2 = k + 1 ) or ( t1 = k + 1 & 1 <= t2 & t2 <= k ) ) by NAT_1:13;

per cases by A181a;

suppose A182: ( t1 in Seg k & t2 = k + 1 ) ; :: thesis:

end;

suppose A189: ( t2 in Seg k & t1 = k + 1 ) ; :: thesis:

end;

for y being object st y in rng (x | (k + 1)) holds
y in the carrier of (Lin (rng (e | (k + 1))))

proof

let y be object ; :: thesis:
assume y in rng (x | (k + 1)) ; :: thesis:
then consider t being object such that
A196: ( t in dom (x | (k + 1)) & y = (x | (k + 1)) . t ) by FUNCT_1:def 3;
len (x | (k + 1)) = k + 1 by FINSEQ_1:59, A58;
then A197: dom (x | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
then A198: y = x . t by A196, FUNCT_1:49;
reconsider t = t as Nat by A196;
A199: ( t in dom x & t in Seg (k + 1) ) by A196, RELAT_1:57;
A200a: len (e | (k + 1)) = k + 1 by FINSEQ_1:59, A30, A58;
then A200: dom (e | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
A208: rng (e | k) c= rng (e | (k + 1))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (e | k) ; :: thesis:
then consider t being object such that
A202: ( t in dom (e | k) & y = (e | k) . t ) by FUNCT_1:def 3;
A203: k < k + 1 by NAT_1:19;
then len (e | k) = k by FINSEQ_1:59, A58, XXREAL_0:2, A30;
then dom (e | k) = Seg k by FINSEQ_1:def 3;
then A204: y = e . t by A202, FUNCT_1:49;
reconsider t = t as Nat by A202;
A205: ( t in dom e & t in Seg k ) by A202, RELAT_1:57;
then ( 1 <= t & t <= k ) by FINSEQ_1:1;
then ( 1 <= t & t <= k + 1 ) by A203, XXREAL_0:2;
then A206: t in Seg (k + 1) ;
then A207: y = (e | (k + 1)) . t by A204, FUNCT_1:49;
t in dom (e | (k + 1)) by RELAT_1:57, A205, A206;
hence y in rng (e | (k + 1)) by A207, FUNCT_1:def 3; :: thesis:

end;

per cases ;

suppose A209: k = 0 ; :: thesis:

then t in Seg (0 + 1) by A196, RELAT_1:57;
then y = x . 1 by A198, TARSKI:def 1, FINSEQ_1:2;
then A212: y = x /. 1 by A1, FINSEQ_3:25, PARTFUN1:def 6;
1 in Seg (len x) by A1;
then A213: 1 in dom e by A30, FINSEQ_1:def 3;
A215: ||.(x /. 1).|| * (e /. 1) = (||.(x /. 1).|| * (1 / ||.(x /. 1).||)) * (x /. 1) by RLVECT_1:def 7, A34
.= 1 * (x /. 1) by A108, XCMPLX_1:87
.= x /. 1 by RLVECT_1:def 8 ;
A216: dom (e | 1) = Seg 1 by A200a, A209, FINSEQ_1:def 3;
A217: 1 in Seg 1 ;
then (e | 1) . 1 = e . 1 by FUNCT_1:49
.= e /. 1 by A213, PARTFUN1:def 6 ;
then e /. 1 in rng (e | 1) by A216, A217, FUNCT_1:def 3;
then y in Lin (rng (e | (k + 1))) by A215, A209, A212, RLSUB_1:21, RLVECT_3:15;
hence y in the carrier of (Lin (rng (e | (k + 1)))) by STRUCT_0:def 5; :: thesis:

end;

suppose A218: k <> 0 ; :: thesis:

k < len x by A58, NAT_1:13;
then consider g being FinSequence of the carrier of H such that
A220: ( g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] & e /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) by A218, A49, NAT_1:14;

per cases ;

suppose A223: t = k + 1 ; :: thesis:

set r = ||.((x /. (1 + k)) - (Sum g)).||;
||.((x /. (1 + k)) - (Sum g)).|| * (e /. (k + 1)) = (||.((x /. (1 + k)) - (Sum g)).|| * (1 / ||.((x /. (1 + k)) - (Sum g)).||)) * ((x /. (1 + k)) - (Sum g)) by RLVECT_1:def 7, A220
.= 1 * ((x /. (1 + k)) - (Sum g)) by XCMPLX_1:87, A218, A220, A123
.= (x /. (1 + k)) - (Sum g) by RLVECT_1:def 8 ;
then A224: x /. (1 + k) = (||.((x /. (1 + k)) - (Sum g)).|| * (e /. (k + 1))) + (Sum g) by RLVECT_4:1;
Seg (k + 1) c= Seg (len e) by A30, A58, FINSEQ_1:5;
then Seg (k + 1) c= dom e by FINSEQ_1:def 3;
then A225: k + 1 in dom e by FINSEQ_1:4;
(e | (k + 1)) . (k + 1) = e . (k + 1) by A223, A196, A197, FUNCT_1:49
.= e /. (k + 1) by A225, PARTFUN1:def 6 ;
then e /. (k + 1) in rng (e | (k + 1)) by A199, A200, FUNCT_1:def 3, A223;
then A226: ||.((x /. (1 + k)) - (Sum g)).|| * (e /. (k + 1)) in Lin (rng (e | (k + 1))) by RLSUB_1:21, RLVECT_3:15;
Lin (rng (e | k)) is Subspace of Lin (rng (e | (k + 1))) by RLVECT_3:20, A208;
then A227a: Sum g in Lin (rng (e | (k + 1))) by RLSUB_1:8, A218, A220, A110;
y = x /. (1 + k) by A223, A198, A199, PARTFUN1:def 6;
hence y in the carrier of (Lin (rng (e | (k + 1)))) by STRUCT_0:def 5, A224, A227a, A226, RLSUB_1:20; :: thesis:

end;

suppose A228: t <> k + 1 ; :: thesis:

M1: ( 1 <= t & t <= k + 1 ) by A196, A197, FINSEQ_1:1;
then t < k + 1 by A228, XXREAL_0:1;
then t <= k by NAT_1:13;
then A229: t in Seg k by M1;
then A230: t in dom (x | k) by A199, RELAT_1:57;
y = (x | k) . t by A198, A229, FUNCT_1:49;
then A231a: y in rng (x | k) by A230, FUNCT_1:def 3;
Lin (rng (e | k)) is Subspace of Lin (rng (e | (k + 1))) by RLVECT_3:20, A208;
then y in Lin (rng (e | (k + 1))) by A231a, RLSUB_1:8, RLVECT_3:15, A57, A58, NAT_1:13;
hence y in the carrier of (Lin (rng (e | (k + 1)))) by STRUCT_0:def 5; :: thesis:

end;

then A232: rng (x | (k + 1)) c= the carrier of (Lin (rng (e | (k + 1)))) ;
for y being object st y in rng (e | (k + 1)) holds
y in the carrier of (Lin (rng (x | (k + 1))))

proof

let y be object ; :: thesis:
assume y in rng (e | (k + 1)) ; :: thesis:
then consider t being object such that
A233: ( t in dom (e | (k + 1)) & y = (e | (k + 1)) . t ) by FUNCT_1:def 3;
len (e | (k + 1)) = k + 1 by FINSEQ_1:59, A58, A30;
then A234: dom (e | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
then A235: y = e . t by A233, FUNCT_1:49;
reconsider t = t as Nat by A233;
A236: ( t in dom e & t in Seg (k + 1) ) by A233, RELAT_1:57;
A237a: len (x | (k + 1)) = k + 1 by FINSEQ_1:59, A58;
then A237: dom (x | (k + 1)) = Seg (k + 1) by FINSEQ_1:def 3;
A245: rng (x | k) c= rng (x | (k + 1))

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng (x | k) ; :: thesis:
then consider t being object such that
A239: ( t in dom (x | k) & y = (x | k) . t ) by FUNCT_1:def 3;
A240: k < k + 1 by NAT_1:19;
then len (x | k) = k by FINSEQ_1:59, A58, XXREAL_0:2;
then dom (x | k) = Seg k by FINSEQ_1:def 3;
then A241: y = x . t by A239, FUNCT_1:49;
reconsider t = t as Nat by A239;
A242: ( t in dom x & t in Seg k ) by A239, RELAT_1:57;
then S1: ( 1 <= t & t <= k ) by FINSEQ_1:1;
then t <= k + 1 by A240, XXREAL_0:2;
then A243: t in Seg (k + 1) by S1;
then A244: y = (x | (k + 1)) . t by A241, FUNCT_1:49;
t in dom (x | (k + 1)) by RELAT_1:57, A242, A243;
hence y in rng (x | (k + 1)) by A244, FUNCT_1:def 3; :: thesis:

end;

per cases ;

suppose A246: k = 0 ; :: thesis:

then t in Seg (0 + 1) by A233, RELAT_1:57;
then A247: y = e . 1 by A235, TARSKI:def 1, FINSEQ_1:2;
A248: 1 in Seg (len e) by A30, A1;
then 1 in dom e by FINSEQ_1:def 3;
then A249: y = e /. 1 by A247, PARTFUN1:def 6;
A250: 1 in dom x by A30, A248, FINSEQ_1:def 3;
A252: dom (x | 1) = Seg 1 by A237a, A246, FINSEQ_1:def 3;
A253: 1 in Seg 1 ;
then (x | 1) . 1 = x . 1 by FUNCT_1:49
.= x /. 1 by A250, PARTFUN1:def 6 ;
then x /. 1 in rng (x | 1) by A252, A253, FUNCT_1:def 3;
then y in Lin (rng (x | (k + 1))) by A34, A246, A249, RLSUB_1:21, RLVECT_3:15;
hence y in the carrier of (Lin (rng (x | (k + 1)))) by STRUCT_0:def 5; :: thesis:

end;

suppose A254: k <> 0 ; :: thesis:

then 1 <= k by NAT_1:14;
then consider g being FinSequence of the carrier of H such that
A256: ( g = (ProjSeq H) . [(x /. (1 + k)),(e | k)] & e /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) by A58, NAT_1:13, A49;

per cases ;

suppose A258: t = k + 1 ; :: thesis:

set r = ||.((x /. (1 + k)) - (Sum g)).||;
A259: e /. (k + 1) = ((1 / ||.((x /. (1 + k)) - (Sum g)).||) * (x /. (1 + k))) - ((1 / ||.((x /. (1 + k)) - (Sum g)).||) * (Sum g)) by RLVECT_1:34, A256;
Seg (k + 1) c= Seg (len x) by A58, FINSEQ_1:5;
then Seg (k + 1) c= dom x by FINSEQ_1:def 3;
then A260: k + 1 in dom x by FINSEQ_1:4;
(x | (k + 1)) . (k + 1) = x . (k + 1) by A233, A234, FUNCT_1:49, A258
.= x /. (k + 1) by A260, PARTFUN1:def 6 ;
then x /. (k + 1) in rng (x | (k + 1)) by A236, A237, FUNCT_1:def 3, A258;
then A261: (1 / ||.((x /. (1 + k)) - (Sum g)).||) * (x /. (k + 1)) in Lin (rng (x | (k + 1))) by RLVECT_3:15, RLSUB_1:21;
Lin (rng (x | k)) is Subspace of Lin (rng (x | (k + 1))) by RLVECT_3:20, A245;
then Sum g in Lin (rng (x | (k + 1))) by A254, A256, A110, A57, A58, NAT_1:13, RLSUB_1:8;
then A262a: (1 / ||.((x /. (1 + k)) - (Sum g)).||) * (Sum g) in Lin (rng (x | (k + 1))) by RLSUB_1:21;
y = e /. (1 + k) by A258, A235, A236, PARTFUN1:def 6;
hence y in the carrier of (Lin (rng (x | (k + 1)))) by STRUCT_0:def 5, A259, A262a, A261, RLSUB_1:23; :: thesis:

end;

suppose A263: t <> k + 1 ; :: thesis:

M1: ( 1 <= t & t <= k + 1 ) by A233, A234, FINSEQ_1:1;
then t < k + 1 by A263, XXREAL_0:1;
then t <= k by NAT_1:13;
then A264: t in Seg k by M1;
then A265: t in dom (e | k) by A236, RELAT_1:57;
y = (e | k) . t by A235, A264, FUNCT_1:49;
then A266a: y in rng (e | k) by A265, FUNCT_1:def 3;
Lin (rng (x | k)) is Subspace of Lin (rng (x | (k + 1))) by RLVECT_3:20, A245;
then y in Lin (rng (x | (k + 1))) by A266a, RLSUB_1:8, A57, A58, NAT_1:13, RLVECT_3:15;
hence y in the carrier of (Lin (rng (x | (k + 1)))) by STRUCT_0:def 5; :: thesis:

end;

then rng (e | (k + 1)) c= the carrier of (Lin (rng (x | (k + 1)))) ;
hence Lin (rng (x | (k + 1))) = Lin (rng (e | (k + 1))) by Th3, A232; :: thesis:

end;

A267: for k being Nat holds S₃[k] from NAT_1:sch 2(A53, A56);
then A268: ( rng (e | (len e)) is OrthonormalFamily of H & e | (len e) is one-to-one & Lin (rng (x | (len x))) = Lin (rng (e | (len e))) ) by A30;
( dom x = Seg (len x) & dom e = Seg (len e) ) by FINSEQ_1:def 3;
hence ( 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)) ) ) ) by A33a, A31, PARTFUN1:def 6, A49, A267, A268, A30; :: thesis: