let cF be complex-valued XFinSequence; ( cF is INT -valued implies Product cF = multint "**" cF )
assume A1:
cF is INT -valued
; Product cF = multint "**" cF
per cases
( len cF = 0 or len cF >= 1 )
by NAT_1:14;
suppose A3:
len cF >= 1
;
Product cF = multint "**" cFA4:
INT = INT /\ COMPLEX
by MEMBERED:1, XBOOLE_1:28;
now for x, y being object st x in INT & y in INT holds
( multint . (x,y) = multcomplex . (x,y) & multint . (x,y) in INT )let x,
y be
object ;
( x in INT & y in INT implies ( multint . (x,y) = multcomplex . (x,y) & multint . (x,y) in INT ) )assume
(
x in INT &
y in INT )
;
( multint . (x,y) = multcomplex . (x,y) & multint . (x,y) in INT )then reconsider X =
x,
Y =
y as
Element of
INT ;
multint . (
x,
y)
= X * Y
by BINOP_2:def 22;
hence
(
multint . (
x,
y)
= multcomplex . (
x,
y) &
multint . (
x,
y)
in INT )
by BINOP_2:def 5, INT_1:def 2;
verum end; hence
Product cF = multint "**" cF
by AFINSQ_2:47, A3, A4, A1;
verum end; end;