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 sequence of REAL such that
A1: f . 1 = RFin . 1 and
A2: for n being Nat st 0 <> n & n < len RFin holds
f . (n + 1) = addreal . ((f . n),(RFin . (n + 1))) and
A3: addreal "**" RFin = f . (len RFin) by FINSOP_1:1;
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) )
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 12;
assume that
A4: 0 <> n and
A5: n < len RFin ; :: thesis: f . (n + 1) = (f . n) + (RFin . (n + 1))
thus f . (n + 1) = addreal . ((f . n1),(RFin . (n1 + 1))) by A2, A4, A5
.= (f . n) + (RFin . (n + 1)) by BINOP_2:def 9 ; :: thesis: verum
end;
hence ( 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, A3, RVSUM_1:def 12; :: thesis: verum