let e1, e2 be FinSequence of H; :: thesis: ( len x = len e1 & rng e1 is OrthonormalFamily of H & e1 is one-to-one & Lin (rng x) = Lin (rng e1) & e1 /. 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)),(e1 | k)] & e1 /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) ) & ( for k being Nat st k <= len x holds
( rng (e1 | k) is OrthonormalFamily of H & e1 | k is one-to-one & Lin (rng (x | k)) = Lin (rng (e1 | k)) ) ) & len x = len e2 & rng e2 is OrthonormalFamily of H & e2 is one-to-one & Lin (rng x) = Lin (rng e2) & e2 /. 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)),(e2 | k)] & e2 /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) ) & ( for k being Nat st k <= len x holds
( rng (e2 | k) is OrthonormalFamily of H & e2 | k is one-to-one & Lin (rng (x | k)) = Lin (rng (e2 | k)) ) ) implies e1 = e2 )
assume that
A2: ( len x = len e1 & rng e1 is OrthonormalFamily of H & e1 is one-to-one & Lin (rng x) = Lin (rng e1) & e1 /. 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)),(e1 | k)] & e1 /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) ) & ( for k being Nat st k <= len x holds
( rng (e1 | k) is OrthonormalFamily of H & e1 | k is one-to-one & Lin (rng (x | k)) = Lin (rng (e1 | k)) ) ) ) and
A3: ( len x = len e2 & rng e2 is OrthonormalFamily of H & e2 is one-to-one & Lin (rng x) = Lin (rng e2) & e2 /. 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)),(e2 | k)] & e2 /. (k + 1) = (1 / ||.((x /. (1 + k)) - (Sum g)).||) * ((x /. (1 + k)) - (Sum g)) ) ) & ( for k being Nat st k <= len x holds
( rng (e2 | k) is OrthonormalFamily of H & e2 | k is one-to-one & Lin (rng (x | k)) = Lin (rng (e2 | k)) ) ) ) ; :: thesis: e1 = e2
A4: ( e1 <> {} & e2 <> {} ) by A1, A2, A3;
defpred S₁[ Nat] means ( 1 <= $1 & $1 <= len x implies e1 | $1 = e2 | $1 );
A6: S₁[ 0 ] ;
A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: S₁[n] ; :: thesis: S₁[n + 1]
assume A9: ( 1 <= n + 1 & n + 1 <= len x ) ; :: thesis: e1 | (n + 1) = e2 | (n + 1)

per cases ( n = 0 or n <> 0 ) ;

suppose A10: n = 0 ; :: thesis: e1 | (n + 1) = e2 | (n + 1)

hence e1 | (n + 1) = <*(e1 . 1)*> by FINSEQ_5:20, A4
.= <*(e1 /. 1)*> by PARTFUN1:def 6, A4, A2, FINSEQ_3:32
.= <*(e2 . 1)*> by A4, PARTFUN1:def 6, A3, A2, FINSEQ_3:32
.= e2 | (n + 1) by A10, FINSEQ_5:20, A4 ;
:: thesis: verum

end;

suppose A11a: n <> 0 ; :: thesis: e1 | (n + 1) = e2 | (n + 1)

then A11: 1 <= n by NAT_1:14;
then consider g1 being FinSequence of H such that
A14: ( g1 = (ProjSeq H) . [(x /. (1 + n)),(e1 | n)] & e1 /. (n + 1) = (1 / ||.((x /. (1 + n)) - (Sum g1)).||) * ((x /. (1 + n)) - (Sum g1)) ) by A2, A9, NAT_1:13;
consider g2 being FinSequence of H such that
A15: ( g2 = (ProjSeq H) . [(x /. (1 + n)),(e2 | n)] & e2 /. (n + 1) = (1 / ||.((x /. (1 + n)) - (Sum g2)).||) * ((x /. (1 + n)) - (Sum g2)) ) by A3, A11, A9, NAT_1:13;
n + 1 in Seg (len x) by A9;
then A17: ( n + 1 in dom e1 & n + 1 in dom e2 ) by A2, A3, FINSEQ_1:def 3;
hence e1 | (n + 1) = (e1 | n) ^ <*(e1 . (n + 1))*> by FINSEQ_5:10
.= (e1 | n) ^ <*(e1 /. (n + 1))*> by A17, PARTFUN1:def 6
.= (e2 | n) ^ <*(e2 . (n + 1))*> by A17, PARTFUN1:def 6, A8, A11a, NAT_1:14, A9, NAT_1:13, A14, A15
.= e2 | (n + 1) by FINSEQ_5:10, A17 ;
:: thesis: verum

end;

end;

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A6, A7);
then A19: e1 | (len x) = e2 | (len x) by A1;
A20: dom e1 = Seg (len x) by A2, FINSEQ_1:def 3;
dom e2 = Seg (len x) by A3, FINSEQ_1:def 3;
hence e1 = e2 by A19, A20; :: thesis: verum