let r be R_eal; :: thesis: for F being FinSequence of ExtREAL holds Sum (F ^ <*r*>) = (Sum F) + r
let F be FinSequence of ExtREAL ; :: thesis: Sum (F ^ <*r*>) = (Sum F) + r
consider f being Function of NAT,ExtREAL such that
A1: ( Sum (F ^ <*r*>) = f . (len (F ^ <*r*>)) & f . 0 = 0 & ( for i being Nat st i < len (F ^ <*r*>) holds
f . (i + 1) = (f . i) + ((F ^ <*r*>) . (i + 1)) ) ) by EXTREAL1:def 2;
consider g being Function of NAT,ExtREAL such that
A2: ( Sum F = g . (len F) & g . 0 = 0 & ( for i being Nat st i < len F holds
g . (i + 1) = (g . i) + (F . (i + 1)) ) ) by EXTREAL1:def 2;
len (F ^ <*r*>) = (len F) + (len <*r*>) by FINSEQ_1:22;
then B1: len (F ^ <*r*>) = (len F) + 1 by FINSEQ_1:39;
then B2: len F < len (F ^ <*r*>) by NAT_1:13;
defpred S₁[ Nat] means ( $1 <= len F implies f . $1 = g . $1 );
A3: S₁[ 0 ] by A1, A2;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
assume A6: k + 1 <= len F ; :: thesis: f . (k + 1) = g . (k + 1)
then A7: k < len F by NAT_1:13;
A9: (F ^ <*r*>) . (k + 1) = F . (k + 1) by A6, FINSEQ_1:64, NAT_1:11;
k < len (F ^ <*r*>) by A7, B1, NAT_1:13;
then f . (k + 1) = (f . k) + ((F ^ <*r*>) . (k + 1)) by A1;
hence f . (k + 1) = g . (k + 1) by A2, A6, A5, A9, NAT_1:13; :: thesis: verum

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A3, A4);
then f . (len F) = g . (len F) ;
then f . ((len F) + 1) = (g . (len F)) + ((F ^ <*r*>) . ((len F) + 1)) by A1, B2;
hence Sum (F ^ <*r*>) = (Sum F) + r by A1, A2, B1, FINSEQ_1:42; :: thesis: verum