let F be XFinSequence; :: thesis: ( F is RAT -valued implies Sum F = addrat "**" F )
assume A1: F is RAT -valued ; :: thesis: Sum F = addrat "**" F
rng F c= COMPLEX by A1, MEMBERED:1;
then A2: F is COMPLEX -valued by RELAT_1:def 19;

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

suppose A3: len F = 0 ; :: thesis: Sum F = addrat "**" F

hence addrat "**" F = 0 by Def8, A1, BINOP_2:3
.= Sum F by Def8, A2, A3, BINOP_2:1 ;
:: thesis: verum

end;

suppose A4: len F >= 1 ; :: thesis: Sum F = addrat "**" F

A5: RAT = RAT /\ COMPLEX by MEMBERED:1, XBOOLE_1:28;

now :: thesis: for x, y being object st x in RAT & y in RAT holds
( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT )

let x, y be object ; :: thesis: ( x in RAT & y in RAT implies ( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT ) )
assume ( x in RAT & y in RAT ) ; :: thesis: ( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT )
then reconsider X = x, Y = y as Element of RAT ;
addrat . (x,y) = X + Y by BINOP_2:def 15;
hence ( addrat . (x,y) = addcomplex . (x,y) & addrat . (x,y) in RAT ) by BINOP_2:def 3, RAT_1:def 2; :: thesis: verum

end;

hence Sum F = addrat "**" F by Th46, A4, A5, A1; :: thesis: verum

end;

end;