set mc = multcomplex ;
consider f being FinSequence of COMPLEX such that
A9: f = F and
A10: Product F = multcomplex $$ f by RVSUM_1:def 14;
set g = [#] (f,(the_unity_wrt multcomplex));
defpred S₁[ Element of NAT ] means multcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt multcomplex)))) is integer ;
A11: 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] )
A12: ([#] (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 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;
hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is integer by A9; :: 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;

assume S₁[k] ; :: thesis: S₁[k + 1]
then reconsider a = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1), b = multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex)))) as integer number by A12;
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;

Seg 0 = {}. NAT ;
then A13: S₁[ 0 ] by BINOP_2:6, SETWISEO:40;
A14: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A13, A11);
consider n being Nat such that
A15: dom f = Seg n by FINSEQ_1:def 2;
A16: multcomplex $$ f = multcomplex $$ ((findom f),([#] (f,(the_unity_wrt multcomplex)))) by SETWOP_2:def 2;
n in NAT by ORDINAL1:def 13;
hence Product F is integer by A10, A16, A15, A14; :: thesis: verum