let F be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL holds Sum (F ^ <*x*>) = (Sum F) + x
let x be Element of ExtREAL ; :: thesis: Sum (F ^ <*x*>) = (Sum F) + x
consider f being Function of NAT ,ExtREAL such that
A1: Sum (F ^ <*x*>) = f . (len (F ^ <*x*>)) and
A2: f . 0 = 0. and
A3: for i being Element of NAT st i < len (F ^ <*x*>) holds
f . (i + 1) = (f . i) + ((F ^ <*x*>) . (i + 1)) by Def5;
A4: len (F ^ <*x*>) = (len F) + (len <*x*>) by FINSEQ_1:35
.= (len F) + 1 by FINSEQ_1:56 ;
for i being Element of NAT st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1))

proof

let i be Element of NAT ; :: thesis: ( i < len F implies f . (i + 1) = (f . i) + (F . (i + 1)) )
assume A5: i < len F ; :: thesis: f . (i + 1) = (f . i) + (F . (i + 1))
then i < len (F ^ <*x*>) by A4, NAT_1:13;
then A6: f . (i + 1) = (f . i) + ((F ^ <*x*>) . (i + 1)) by A3;
( 1 <= i + 1 & i + 1 <= len F ) by A5, INT_1:20, NAT_1:11;
then i + 1 in Seg (len F) by FINSEQ_1:3;
then i + 1 in dom F by FINSEQ_1:def 3;
hence f . (i + 1) = (f . i) + (F . (i + 1)) by A6, FINSEQ_1:def 7; :: thesis: verum

end;

then A7: Sum F = f . (len F) by A2, Def5;
len F < len (F ^ <*x*>) by A4, NAT_1:13;
then f . ((len F) + 1) = (f . (len F)) + ((F ^ <*x*>) . ((len F) + 1)) by A3;
hence Sum (F ^ <*x*>) = (Sum F) + x by A1, A4, A7, FINSEQ_1:59; :: thesis: verum