let a be R_eal; 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
by FINSEQ_1:40
;
hence
Sum <*a*> = a
; verum