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 13;

now

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 Def11;
A3: (ProjFinSeq x0) . 1 = (accum (ProjFinSeq x0)) . 1 by Def11;
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 ) );
A5: len (ProjFinSeq x0) = n by Def12;
A6: 0 + 1 <= len (ProjFinSeq x0) by A1, NAT_1:13;
A7: 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 13;
assume A8: 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
A9: 1 <= i and
A10: i <= len (ProjFinSeq x0) and
A11: 1 <= k + 1 and
A12: 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, A11, A12, FINSEQ_4:24;
reconsider i2 = i as Element of NAT by ORDINAL1:def 13;
A13: (accum (ProjFinSeq x0)) /. (k + 1) = (accum (ProjFinSeq x0)) . (k + 1) by A2, A11, A12, FINSEQ_4:24;

now

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

case A14: 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 ;
A15: (ProjFinSeq x0) /. (k + 1) = (ProjFinSeq x0) . (k + 1) by A11, A12, FINSEQ_4:24
.= |(x0,(Base_FinSeq n2,(k + 1)))| * (Base_FinSeq n2,(k + 1)) by A5, A11, A12, Def12 ;
A16: k < k + 1 by XREAL_1:31;
then A17: k < len (ProjFinSeq x0) by A12, XXREAL_0:2;
then r = ((accum (ProjFinSeq x0)) /. k) + ((ProjFinSeq x0) /. (k + 1)) by Def11, A14;
then A18: r . i = (r2 . i) + (r3 . i) by RVSUM_1:27;

A19: now

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

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

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

then A22: i <= k by NAT_1:13;
((ProjFinSeq x0) /. (k + 1)) . i = |(x0,(Base_FinSeq n2,(k + 1)))| * ((Base_FinSeq n2,(k2 + 1)) . i2) by A15, RVSUM_1:66
.= |(x0,(Base_FinSeq n2,(k + 1)))| * 0 by A5, A9, A10, A21, MATRIXR2:76 ;
hence ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i by A8, A9, A10, A13, A14, A17, A18, A22; :: thesis: verum

end;

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

then A24: ((accum (ProjFinSeq x0)) /. k) . i = 0 by A8, A9, A10, A14, A16, A17;
((ProjFinSeq x0) /. (k + 1)) . i = |(x0,(Base_FinSeq n2,(k + 1)))| * ((Base_FinSeq n2,(k2 + 1)) . i2) by A15, RVSUM_1:66
.= |(x0,(Base_FinSeq n2,(k + 1)))| * 1 by A5, A9, A10, A23, MATRIXR2:75
.= x0 . (k + 1) by A5, A11, A12, Th32 ;
hence ((accum (ProjFinSeq x0)) /. (k + 1)) . i = x0 . i by A2, A9, A10, A18, A23, A24, FINSEQ_4:24; :: thesis: verum

end;

end;

end;

now

assume A25: i > k + 1 ; :: thesis: ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0
then A26: i > k by A16, XXREAL_0:2;
((ProjFinSeq x0) /. (k + 1)) . i = |(x0,(Base_FinSeq n2,(k + 1)))| * ((Base_FinSeq n2,(k2 + 1)) . i2) by A15, RVSUM_1:66
.= |(x0,(Base_FinSeq n2,(k + 1)))| * 0 by A5, A9, A10, A25, MATRIXR2:76
.= 0 ;
hence ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 by A8, A9, A10, A13, A14, A17, A18, A26; :: 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 A19; :: 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 A27: k + 1 <= 0 + 1 by NAT_1:13;
then A28: k = 0 by XREAL_1:8;

A29: now

assume A30: i > 0 + 1 ; :: thesis: ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0
(accum (ProjFinSeq x0)) /. 1 = (ProjFinSeq x0) . 1 by A6, A2, A3, FINSEQ_4:24;
then ((accum (ProjFinSeq x0)) /. 1) . i = (|(x0,(Base_FinSeq n2,1))| * (Base_FinSeq n2,1)) . i by A6, A5, Def12
.= |(x0,(Base_FinSeq n2,1))| * ((Base_FinSeq n2,1) . i2) by RVSUM_1:66
.= |(x0,(Base_FinSeq n2,1))| * 0 by A5, A10, A30, MATRIXR2:76
.= 0 ;
hence ((accum (ProjFinSeq x0)) /. (k + 1)) . i = 0 by A28; :: thesis: verum

end;

A31: now

assume i <= 0 + 1 ; :: thesis: ((accum (ProjFinSeq x0)) /. (0 + 1)) . i = x0 . i
then A32: i = 1 by A9, XXREAL_0:1;
(accum (ProjFinSeq x0)) /. 1 = (ProjFinSeq x0) . 1 by A6, A2, A3, FINSEQ_4:24;
then ((accum (ProjFinSeq x0)) /. 1) . 1 = (|(x0,(Base_FinSeq n2,1))| * (Base_FinSeq n2,1)) . 1 by A6, A5, Def12
.= |(x0,(Base_FinSeq n2,1))| * ((Base_FinSeq n2,1) . 1) by RVSUM_1:66
.= |(x0,(Base_FinSeq n2,1))| * 1 by A6, A5, MATRIXR2:75
.= x0 . 1 by A6, A5, Th32 ;
hence ((accum (ProjFinSeq x0)) /. (0 + 1)) . i = x0 . i by A32; :: thesis: verum

end;

k <= 0 by A27, XREAL_1:8;
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 A31, A29; :: 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 ;
A33: len x0 = n by FINSEQ_1:def 18;
then A34: len x0 = len r4 by FINSEQ_1:def 18;
A35: S₁[ 0 ] ;
A36: for k being Nat holds S₁[k] from NAT_1:sch 2(A35, A7);
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
A37: 1 <= i and
A38: i <= len r4 ; :: thesis: ((accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0))) . i = x0 . i
A39: i <= len (ProjFinSeq x0) by A5, A38, FINSEQ_1:def 18;
1 <= len (ProjFinSeq x0) by A5, A33, A34, A37, A38, XXREAL_0:2;
hence ((accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0))) . i = x0 . i by A36, A37, A39; :: thesis: verum

end;

then x0 = (accum (ProjFinSeq x0)) /. (len (ProjFinSeq x0)) by A34, FINSEQ_1:18;
hence x0 = (accum (ProjFinSeq x0)) . (len (ProjFinSeq x0)) by A6, A2, FINSEQ_4:24; :: thesis: verum

end;

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

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

end;

end;

end;

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