let cF be complex-valued XFinSequence; :: thesis: ( cF is natural-valued implies Product cF = multnat "**" cF )

assume cF is natural-valued ; :: thesis: Product cF = multnat "**" cF

then rng cF c= NAT by VALUED_0:def 6;

then A1: cF is NAT -valued by RELAT_1:def 19;

assume cF is natural-valued ; :: thesis: Product cF = multnat "**" cF

then rng cF c= NAT by VALUED_0:def 6;

then A1: cF is NAT -valued by RELAT_1:def 19;

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

end;

suppose A2:
len cF = 0
; :: thesis: Product cF = multnat "**" cF

hence multnat "**" cF =
the_unity_wrt multcomplex
by BINOP_2:6, BINOP_2:10, AFINSQ_2:def 8, A1

.= Product cF by AFINSQ_2:def 8, A2 ;

:: thesis: verum

end;.= Product cF by AFINSQ_2:def 8, A2 ;

:: thesis: verum

suppose A3:
len cF >= 1
; :: thesis: Product cF = multnat "**" cF

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

end;now :: thesis: for x, y being object st x in NAT & y in NAT holds

( multnat . (x,y) = multcomplex . (x,y) & multnat . (x,y) in NAT )

hence
Product cF = multnat "**" cF
by AFINSQ_2:47, A3, A4, A1; :: thesis: verum( multnat . (x,y) = multcomplex . (x,y) & multnat . (x,y) in NAT )

let x, y be object ; :: thesis: ( x in NAT & y in NAT implies ( multnat . (x,y) = multcomplex . (x,y) & multnat . (x,y) in NAT ) )

assume ( x in NAT & y in NAT ) ; :: thesis: ( multnat . (x,y) = multcomplex . (x,y) & multnat . (x,y) in NAT )

then reconsider X = x, Y = y as Element of NAT ;

multnat . (x,y) = X * Y by BINOP_2:def 24;

hence ( multnat . (x,y) = multcomplex . (x,y) & multnat . (x,y) in NAT ) by BINOP_2:def 5, ORDINAL1:def 12; :: thesis: verum

end;assume ( x in NAT & y in NAT ) ; :: thesis: ( multnat . (x,y) = multcomplex . (x,y) & multnat . (x,y) in NAT )

then reconsider X = x, Y = y as Element of NAT ;

multnat . (x,y) = X * Y by BINOP_2:def 24;

hence ( multnat . (x,y) = multcomplex . (x,y) & multnat . (x,y) in NAT ) by BINOP_2:def 5, ORDINAL1:def 12; :: thesis: verum