let F be XFinSequence; :: thesis: ( F is natural-valued implies Sum F = addnat "**" F )
assume A1: F is natural-valued ; :: thesis: Sum F = addnat "**" F
then rng F c= NAT by VALUED_0:def 6;
then A2: F is NAT -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 = addnat "**" F

hence addnat "**" F = 0 by Def8, A2, BINOP_2:5
.= Sum F by Def8, A3, A4, BINOP_2:1 ;
:: thesis: verum

end;

suppose A5: len F >= 1 ; :: thesis: Sum F = addnat "**" F

A6: NAT = NAT /\ COMPLEX by MEMBERED:1, XBOOLE_1:28;

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

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

end;

hence Sum F = addnat "**" F by Th46, A5, A6, A2; :: thesis: verum

end;

end;