let F be FinSequence of REAL ; :: thesis: ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) )

per cases ( len F = 0 or len F > 0 ) ;

suppose A1: len F = 0 ; :: thesis: ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) )

set f = NAT --> 0 ;
A3: for i being Nat holds (NAT --> 0 ) . i = 0

proof

let i be Nat; :: thesis: (NAT --> 0 ) . i = 0
i in NAT by ORDINAL1:def 13;
hence (NAT --> 0 ) . i = 0 by FUNCOP_1:13; :: thesis: verum

end;

A4: for i being Nat st i < len F holds
(NAT --> 0 ) . (i + 1) = ((NAT --> 0 ) . i) + (F . (i + 1)) by A1;
A5: Sum F = 0 by A1, PROB_3:67
.= (NAT --> 0 ) . (len F) by A3 ;
(NAT --> 0 ) . 0 = 0 by A3;
hence ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) ) by A4, A5; :: thesis: verum

end;

suppose A6: len F > 0 ; :: thesis: ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) )

then A7: len F >= 1 by NAT_1:14;
then consider f being Real_Sequence such that
A8: ( f . 1 = F . 1 & ( for i being Nat st 0 <> i & i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) ) by PROB_3:68;
consider f1 being Real_Sequence such that
A9: for n being Nat holds
( f1 . 0 = 0 & ( n <> 0 & n <= len F implies f1 . n = f . n ) & ( n > len F implies f1 . n = 0 ) ) by Th6;
A10: for i being Nat st i < len F holds
f1 . (i + 1) = (f1 . i) + (F . (i + 1))

proof

let i be Nat; :: thesis: ( i < len F implies f1 . (i + 1) = (f1 . i) + (F . (i + 1)) )
assume A11: i < len F ; :: thesis: f1 . (i + 1) = (f1 . i) + (F . (i + 1))
set r = F . (i + 1);

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

suppose i = 0 ; :: thesis: f1 . (i + 1) = (f1 . i) + (F . (i + 1))

hence f1 . (i + 1) = (f1 . i) + (F . (i + 1)) by A7, A8, A9; :: thesis: verum

end;

suppose A12: i <> 0 ; :: thesis: f1 . (i + 1) = (f1 . i) + (F . (i + 1))

( i + 1 <> 0 & i + 1 <= len F ) by A11, NAT_1:13;
hence f1 . (i + 1) = f . (i + 1) by A9
.= (f . i) + (F . (i + 1)) by A8, A11, A12
.= (f1 . i) + (F . (i + 1)) by A9, A11, A12 ;
:: thesis: verum

end;

end;

end;

Sum F = f1 . (len F) by A6, A8, A9;
hence ex f being Real_Sequence st
( f . 0 = 0 & ( for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) ) & Sum F = f . (len F) ) by A9, A10; :: thesis: verum

end;

end;