let RFin be FinSequence of REAL ; :: thesis: ( len RFin >= 1 implies ex f being Real_Sequence st
( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds
f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) ) )
assume len RFin >= 1 ; :: thesis: ex f being Real_Sequence st
( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds
f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) )
then consider f being Function of NAT ,REAL such that
A1: ( f . 1 = RFin . 1 & ( for n being Element of NAT st 0 <> n & n < len RFin holds
f . (n + 1) = addreal . (f . n),(RFin . (n + 1)) ) & addreal "**" RFin = f . (len RFin) ) by FINSOP_1:2;
A2: for n being Nat st 0 <> n & n < len RFin holds
f . (n + 1) = (f . n) + (RFin . (n + 1))

proof

let n be Nat; :: thesis: ( 0 <> n & n < len RFin implies f . (n + 1) = (f . n) + (RFin . (n + 1)) )
reconsider n1 = n as Element of NAT by ORDINAL1:def 13;
assume A3: ( 0 <> n & n < len RFin ) ; :: thesis: f . (n + 1) = (f . n) + (RFin . (n + 1))
then n + 1 in Seg (len RFin) by FINSEQ_3:12;
then n + 1 in dom RFin by FINSEQ_1:def 3;
then A4: ( f . n1 is Real & RFin . (n1 + 1) is Real ) by FINSEQ_2:13;
thus f . (n + 1) = addreal . (f . n1),(RFin . (n1 + 1)) by A1, A3
.= (f . n) + (RFin . (n + 1)) by A4, BINOP_2:def 9 ; :: thesis: verum

end;

take f ; :: thesis: ( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds
f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) )
thus ( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds
f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) ) by A1, A2, RVSUM_1:def 13; :: thesis: verum