consider f being FinSequence of COMPLEX such that
A1: ( f = F & Product F = multcomplex $$ f ) by RVSUM_1:def 14;
A2: rng f c= INT by A1, VALUED_0:def 5;
then reconsider f' = f as FinSequence of INT by FINSEQ_1:def 4;
set mc = multcomplex ;
set mr = multint ;
A3: multcomplex $$ f = multcomplex $$ (findom f),([#] f,(the_unity_wrt multcomplex )) by SETWOP_2:def 2;
consider n being Nat such that
A4: dom f = Seg n by FINSEQ_1:def 2;
AA: n in NAT by ORDINAL1:def 13;
defpred S₁[ Element of NAT ] means multcomplex $$ (finSeg F),([#] f,(the_unity_wrt multcomplex )) is integer ;
Seg 0 = {}. NAT ;
then A5: S₁[ 0 ] by BINOP_2:6, SETWISEO:40;
set g = [#] f,(the_unity_wrt multcomplex );
A6: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
A8: ([#] f,(the_unity_wrt multcomplex )) . (k + 1) is integer

proof

per cases ( k + 1 in dom f or not k + 1 in dom f ) ;

suppose A9: k + 1 in dom f ; :: thesis: ([#] f,(the_unity_wrt multcomplex )) . (k + 1) is integer

then ([#] f,(the_unity_wrt multcomplex )) . (k + 1) = f . (k + 1) by SETWOP_2:22;
then ([#] f,(the_unity_wrt multcomplex )) . (k + 1) in rng f by A9, FUNCT_1:12;
hence ([#] f,(the_unity_wrt multcomplex )) . (k + 1) is integer by A2; :: thesis: verum

end;

suppose not k + 1 in dom f ; :: thesis: ([#] f,(the_unity_wrt multcomplex )) . (k + 1) is integer

hence ([#] f,(the_unity_wrt multcomplex )) . (k + 1) is integer by BINOP_2:6, SETWOP_2:22; :: thesis: verum

end;

end;

end;

reconsider a = ([#] f,(the_unity_wrt multcomplex )) . (k + 1), b = multcomplex $$ (finSeg k),([#] f,(the_unity_wrt multcomplex )) as integer number by A7, A8;
not k + 1 in Seg k by FINSEQ_3:9;
then multcomplex $$ ((finSeg k) \/ {.(k + 1).}),([#] f,(the_unity_wrt multcomplex )) = multcomplex . (multcomplex $$ (finSeg k),([#] f,(the_unity_wrt multcomplex ))),(([#] f,(the_unity_wrt multcomplex )) . (k + 1)) by SETWOP_2:4
.= b * a by BINOP_2:def 5 ;
hence S₁[k + 1] by FINSEQ_1:11; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A6);
hence Product F is integer by A1, A4, A3, AA; :: thesis: verum