let F be XFinSequence; ( F is natural-valued implies Sum F = addnat "**" F )
assume A1:
F is natural-valued
; 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 A5:
len F >= 1
;
Sum F = addnat "**" FA6:
NAT = NAT /\ COMPLEX
by MEMBERED:1, XBOOLE_1:28;
now 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 ;
( 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 )
;
( 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;
verum end; hence
Sum F = addnat "**" F
by Th46, A5, A6, A2;
verum end; end;