let a be R_eal; :: thesis: Sum <*a*> = a
consider f being sequence of ExtREAL such that
A1: ( Sum <*a*> = f . (len <*a*>) & f . 0 = 0. & ( for i being Nat st i < len <*a*> holds
f . (i + 1) = (f . i) + (<*a*> . (i + 1)) ) ) by EXTREAL1:def 2;
A2: len <*a*> = 1 by FINSEQ_1:39;
f . (0 + 1) = (f . 0) + (<*a*> . (0 + 1)) by A1
.= 0 + a by A1, FINSEQ_1:40 ;
hence Sum <*a*> = a by A1, A2, XXREAL_3:4; :: thesis: verum