let F be XFinSequence; :: thesis: ( F is real-valued implies Sum F = addreal "**" F )
assume A1: F is real-valued ; :: thesis: Sum F = addreal "**" F
then rng F c= REAL by VALUED_0:def 3;
then A3: F is REAL -valued by RELAT_1:def 19;
rng F c= COMPLEX by MEMBERED:1, A1;
then A4: F is COMPLEX -valued by RELAT_1:def 19;

per cases ( len F = 0 or len F >= 1 ) by NAT_1:14;

suppose A5: len F = 0 ; :: thesis: Sum F = addreal "**" F

hence addreal "**" F = 0 by BINOP_2:2, Def9, A3
.= Sum F by Def9, A4, A5, BINOP_2:1 ;
:: thesis: verum

end;

suppose A6: len F >= 1 ; :: thesis: Sum F = addreal "**" F

A7: REAL = REAL /\ COMPLEX by XBOOLE_1:28, MEMBERED:1;

now

let x, y be set ; :: thesis: ( x in REAL & y in REAL implies ( addreal . x,y = addcomplex . x,y & addreal . x,y in REAL ) )
assume ( x in REAL & y in REAL ) ; :: thesis: ( addreal . x,y = addcomplex . x,y & addreal . x,y in REAL )
then reconsider X = x, Y = y as Element of REAL ;
addreal . x,y = X + Y by BINOP_2:def 9;
hence ( addreal . x,y = addcomplex . x,y & addreal . x,y in REAL ) by BINOP_2:def 3; :: thesis: verum

end;

hence Sum F = addreal "**" F by Th60, A6, A7, A3; :: thesis: verum

end;

end;