let a be R_eal; :: thesis: Sum <*a*> = a
set F = <*a*>;
consider f being sequence of ExtREAL such that
A1: Sum <*a*> = f . (len <*a*>) and
A2: f . 0 = 0. and
A3: for i being Nat st i < len <*a*> holds
f . (i + 1) = (f . i) + (<*a*> . (i + 1)) by Def2;
A4: f . (0 + 1) = (f . 0) + (<*a*> . (0 + 1)) by A3;
Sum <*a*> = f . 1 by A1, FINSEQ_1:39;
then Sum <*a*> = <*a*> . 1 by A2, A4, XXREAL_3:4
.= a ;
hence Sum <*a*> = a ; :: thesis: verum