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 A2: F is REAL -valued by RELAT_1:def 19;
rng F c= COMPLEX by A1, MEMBERED:1;
then A3: F is COMPLEX -valued by RELAT_1:def 19;
per cases ( len F = 0 or len F >= 1 ) by NAT_1:14;
suppose A4: len F = 0 ; :: thesis: Sum F = addreal "**" F
hence addreal "**" F = 0 by Def8, A2, BINOP_2:2
.= Sum F by Def8, A3, A4, BINOP_2:1 ;
:: thesis: verum
end;
suppose A5: len F >= 1 ; :: thesis: Sum F = addreal "**" F
A6: REAL = REAL /\ COMPLEX by MEMBERED:1, XBOOLE_1:28;
now :: thesis: for x, y being object st x in REAL & y in REAL holds
( addreal . (x,y) = addcomplex . (x,y) & addreal . (x,y) in REAL )
let x, y be object ; :: 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, XREAL_0:def 1; :: thesis: verum
end;
hence Sum F = addreal "**" F by Th46, A5, A6, A2; :: thesis: verum
end;
end;