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))

f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) ) by A1, A3, RVSUM_1:def 12; :: thesis: verum

( 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

hence
( f . 1 = RFin . 1 & ( for n being Nat st 0 <> n & n < len RFin holds
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;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

f . (n + 1) = (f . n) + (RFin . (n + 1)) ) & Sum RFin = f . (len RFin) ) by A1, A3, RVSUM_1:def 12; :: thesis: verum