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 = seq_const 0;
A2: for i being Nat st i < len F holds
(seq_const 0) . (i + 1) = ((seq_const 0) . i) + (F . (i + 1)) by A1;
A3: for i being Nat holds (seq_const 0) . i = 0 by SEQ_1:57;
then A4: (seq_const 0) . 0 = 0 ;
Sum F = 0 by A1, PROB_3:62
.= (seq_const 0) . (len F) 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 A2, A4; :: thesis: verum

end;

suppose A5: 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 consider f being Real_Sequence such that
A6: f . 1 = F . 1 and
A7: for i being Nat st 0 <> i & i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) and
A8: Sum F = f . (len F) by NAT_1:14, PROB_3:63;
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: len F >= 1 by A5, NAT_1:14;
A11: 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 A12: 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 A10, A6, A9; :: thesis: verum

end;

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

i + 1 <= len F by A12, NAT_1:13;
hence f1 . (i + 1) = f . (i + 1) by A9
.= (f . i) + (F . (i + 1)) by A7, A12, A13
.= (f1 . i) + (F . (i + 1)) by A9, A12, A13 ;
:: thesis: verum

end;

end;

end;

Sum F = f1 . (len F) by A5, 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, A11; :: thesis: verum

end;

end;