let a be R_eal; :: thesis: Sum <*a*> = a
set F = <*a*>;
consider f being Function of NAT ,ExtREAL such that
A1: Sum <*a*> = f . (len <*a*>) and
A2: f . 0 = 0. and
A3: for i being Element of NAT st i < len <*a*> holds
f . (i + 1) = (f . i) + (<*a*> . (i + 1)) by Def5;
len <*a*> = 1 by FINSEQ_1:56;
then ( Sum <*a*> = f . 1 & f . (0 + 1) = (f . 0 ) + (<*a*> . (0 + 1)) ) by A1, A3;
then Sum <*a*> = <*a*> . 1 by A2, XXREAL_3:4
.= a by FINSEQ_1:57 ;
hence Sum <*a*> = a ; :: thesis: verum