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 sequence of ExtREAL such that
A1: Sum (F ^ <*x*>) = f . (len (F ^ <*x*>)) and
A2: f . 0 = 0. and
A3: for i being Nat st i < len (F ^ <*x*>) holds
f . (i + 1) = (f . i) + ((F ^ <*x*>) . (i + 1)) by EXTREAL1:def 2;
A4: len (F ^ <*x*>) = (len F) + (len <*x*>) by FINSEQ_1:22
.= (len F) + 1 by FINSEQ_1:39 ;
for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1))

proof

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

end;

then A8: Sum F = f . (len F) by A2, EXTREAL1:def 2;
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, A8, FINSEQ_1:42; :: thesis: verum