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 by FINSEQ_1:40 ;

hence Sum <*a*> = a ; :: thesis: verum

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 ; :: thesis: verum