let n be Nat; :: thesis: for x0 being Element of REAL n holds x0 = Sum (ProjFinSeq x0)
let x0 be Element of REAL n; :: thesis: x0 = Sum (ProjFinSeq x0)
set f = ProjFinSeq x0;
reconsider n2 = n as Element of NAT by ORDINAL1:def 12;

now :: thesis: ( ( len (ProjFinSeq x0) > 0 & x0 = (accum (ProjFinSeq x0)) . (len (ProjFinSeq x0)) ) or ( len (ProjFinSeq x0) <= 0 & x0 = 0* n ) )

per cases ( len (ProjFinSeq x0) > 0 or len (ProjFinSeq x0) <= 0 ) ;

case A1: len (ProjFinSeq x0) > 0 ; :: thesis: x0 = (accum (ProjFinSeq x0)) . (len (ProjFinSeq x0))

set g2 = accum (ProjFinSeq x0);
A2: len (ProjFinSeq x0) = len (accum (ProjFinSeq x0)) by Def10;
A3: (ProjFinSeq x0) . 1 = (accum (ProjFinSeq x0)) . 1 by Def10;
defpred S₁[ Nat] means for i being Nat st 1 <= i & i <= len (ProjFinSeq x0) & 1 <= $1 & $1 <= len (ProjFinSeq x0) holds
( ( i <= $1 implies ((accum (ProjFinSeq x0)) /. $1) . i = x0 . i ) & ( i > $1 implies ((accum (ProjFinSeq x0)) /. $1) . i = 0 ) );
A4: len (ProjFinSeq x0) = n by Def12;
A5: 0 + 1 <= len (ProjFinSeq x0) by A1, NAT_1:13;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
reconsider k2 = k as Element of NAT by ORDINAL1:def 12;
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
for i being Nat st 1 <= i & i <= len (ProjFinSeq x0) & 1 <= k + 1 & k + 1 <= len (ProjFinSeq x0) holds
( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len (ProjFinSeq x0) & 1 <= k + 1 & k + 1 <= len (ProjFinSeq x0) implies ( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) ) )
assume that
A8: 1 <= i and
A9: i <= len (ProjFinSeq x0) and
A10: 1 <= k + 1 and
A11: k + 1 <= len (ProjFinSeq x0) ; :: thesis: ( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )
(accum (ProjFinSeq x0)) /. (k + 1) is Element of REAL n ;
then reconsider r = (accum (ProjFinSeq x0)) . (k + 1) as Element of REAL n by A2, A10, A11, FINSEQ_4:15;
reconsider i2 = i as Element of NAT by ORDINAL1:def 12;
A12: (accum (ProjFinSeq x0)) /. (k + 1) = (accum (ProjFinSeq x0)) . (k + 1) by A2, A10, A11, FINSEQ_4:15;

now :: thesis: ( ( 1 <= k & ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) ) or ( k < 1 & ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) ) )

per cases ( 1 <= k or k < 1 ) ;

case A13: 1 <= k ; :: thesis: ( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )

reconsider r3 = (ProjFinSeq x0) /. (k + 1) as Element of REAL n ;
reconsider r2 = (accum (ProjFinSeq x0)) /. k as Element of REAL n ;
A14: (ProjFinSeq x0) /. (k + 1) = (ProjFinSeq x0) . (k + 1) by A10, A11, FINSEQ_4:15
.= |(x0,(Base_FinSeq (n2,(k + 1))))| * (Base_FinSeq (n2,(k + 1))) by A4, A10, A11, Def12 ;
A15: k < k + 1 by XREAL_1:29;
then A16: k < len (ProjFinSeq x0) by A11, XXREAL_0:2;
then r = ((accum (ProjFinSeq x0)) /. k) + ((ProjFinSeq x0) /. (k + 1)) by Def10, A13;
then A17: r . i = (r2 . i) + (r3 . i) by RVSUM_1:11;

A18: now :: thesis: ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i )

assume A19: i <= k + 1 ; :: thesis: ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i

per cases ( i < k + 1 or i = k + 1 ) by A19, XXREAL_0:1;

suppose A20: i < k + 1 ; :: thesis: ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i

then A21: i <= k by NAT_1:13;
((ProjFinSeq x0) /. (k + 1)) . i = |(x0,(Base_FinSeq (n2,(k + 1))))| * ((Base_FinSeq (n2,(k2 + 1))) . i2) by A14, RVSUM_1:44
.= |(x0,(Base_FinSeq (n2,(k + 1))))| * 0 by A4, A8, A9, A20, MATRIXR2:76 ;
hence ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i by A7, A8, A9, A12, A13, A16, A17, A21; :: thesis: verum

end;

suppose A22: i = k + 1 ; :: thesis: ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i

then A23: ((accum (ProjFinSeq x0)) /. k) . i = 0 by A7, A8, A9, A13, A15, A16;
((ProjFinSeq x0) /. (k + 1)) . i = |(x0,(Base_FinSeq (n2,(k + 1))))| * ((Base_FinSeq (n2,(k2 + 1))) . i2) by A14, RVSUM_1:44
.= |(x0,(Base_FinSeq (n2,(k + 1))))| * 1 by A4, A8, A9, A22, MATRIXR2:75
.= x0 . (k + 1) by A4, A10, A11, Th29 ;
hence ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i by A2, A8, A9, A17, A22, A23, FINSEQ_4:15; :: thesis: verum

end;

end;

end;

now :: thesis: ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 )

assume A24: i > k + 1 ; :: thesis: ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0
then A25: i > k by A15, XXREAL_0:2;
((ProjFinSeq x0) /. (k + 1)) . i = |(x0,(Base_FinSeq (n2,(k + 1))))| * ((Base_FinSeq (n2,(k2 + 1))) . i2) by A14, RVSUM_1:44
.= |(x0,(Base_FinSeq (n2,(k + 1))))| * 0 by A4, A8, A9, A24, MATRIXR2:76
.= 0 ;
hence ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 by A7, A8, A9, A12, A13, A16, A17, A25; :: thesis: verum

end;

hence ( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) ) by A18; :: thesis: verum

end;

case k < 1 ; :: thesis: ( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) )

then A26: k + 1 <= 0 + 1 by NAT_1:13;
then A27: k = 0 by XREAL_1:6;

A28: now :: thesis: ( i > 0 + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 )

assume A29: i > 0 + 1 ; :: thesis: ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0
(accum (ProjFinSeq x0)) /. 1 = (ProjFinSeq x0) . 1 by A5, A2, A3, FINSEQ_4:15;
then ((accum (ProjFinSeq x0)) /. 1) . i = (|(x0,(Base_FinSeq (n2,1)))| * (Base_FinSeq (n2,1))) . i by A5, A4, Def12
.= |(x0,(Base_FinSeq (n2,1)))| * ((Base_FinSeq (n2,1)) . i2) by RVSUM_1:44
.= |(x0,(Base_FinSeq (n2,1)))| * 0 by A4, A9, A29, MATRIXR2:76
.= 0 ;
hence ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 by A27; :: thesis: verum

end;

A30: now :: thesis: ( i <= 0 + 1 implies ((accum (ProjFinSeq x0)) /. (0 + 1)) . i = x0 . i )

assume i <= 0 + 1 ; :: thesis: ((accum (ProjFinSeq x0)) /. (0 + 1)) . i = x0 . i
then A31: i = 1 by A8, XXREAL_0:1;
(accum (ProjFinSeq x0)) /. 1 = (ProjFinSeq x0) . 1 by A5, A2, A3, FINSEQ_4:15;
then ((accum (ProjFinSeq x0)) /. 1) . 1 = (|(x0,(Base_FinSeq (n2,1)))| * (Base_FinSeq (n2,1))) . 1 by A5, A4, Def12
.= |(x0,(Base_FinSeq (n2,1)))| * ((Base_FinSeq (n2,1)) . 1) by RVSUM_1:44
.= |(x0,(Base_FinSeq (n2,1)))| * 1 by A5, A4, MATRIXR2:75
.= x0 . 1 by A5, A4, Th29 ;
hence ((accum (ProjFinSeq x0)) /. (0 + 1)) . i = x0 . i by A31; :: thesis: verum

end;

k <= 0 by A26, XREAL_1:6;
hence ( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) ) by A30, A28; :: thesis: verum

end;

end;

end;

hence ( ( i <= k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i ) & ( i > k + 1 implies ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 ) ) ; :: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

reconsider r4 = (accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0)) as Element of REAL n ;
A32: len x0 = n by CARD_1:def 7;
then A33: len x0 = len r4 by CARD_1:def 7;
A34: S₁[ 0 ] ;
A35: for k being Nat holds S₁[k] from NAT_1:sch 2(A34, A6);
for i being Nat st 1 <= i & i <= len r4 holds
((accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0))) . i = x0 . i

proof

let i be Nat; :: thesis: ( 1 <= i & i <= len r4 implies ((accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0))) . i = x0 . i )
assume that
A36: 1 <= i and
A37: i <= len r4 ; :: thesis: ((accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0))) . i = x0 . i
A38: i <= len (ProjFinSeq x0) by A4, A37, CARD_1:def 7;
1 <= len (ProjFinSeq x0) by A4, A32, A33, A36, A37, XXREAL_0:2;
hence ((accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0))) . i = x0 . i by A35, A36, A38; :: thesis: verum

end;

then x0 = (accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0)) by A33, FINSEQ_1:14;
hence x0 = (accum (ProjFinSeq x0)) . (len (ProjFinSeq x0)) by A5, A2, FINSEQ_4:15; :: thesis: verum

end;

case len (ProjFinSeq x0) <= 0 ; :: thesis: x0 = 0* n

then A39: n = 0 by Def12;
then x0 = <*> REAL ;
hence x0 = 0* n by A39; :: thesis: verum

end;

end;

end;

hence x0 = Sum (ProjFinSeq x0) by Def11; :: thesis: verum