set mc = multcomplex ;

consider f being FinSequence of COMPLEX such that

A9: f = F and

A10: Product F = multcomplex $$ f by RVSUM_1:def 13;

set g = [#] (f,(the_unity_wrt multcomplex));

defpred S_{1}[ Nat] means multcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt multcomplex)))) is integer ;

A11: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

then A13: S_{1}[ 0 ]
by BINOP_2:6, SETWISEO:31;

A14: for n being Nat holds S_{1}[n]
from NAT_1:sch 2(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;

thus Product F is integer by A10, A16, A15, A14; :: thesis: verum

consider f being FinSequence of COMPLEX such that

A9: f = F and

A10: Product F = multcomplex $$ f by RVSUM_1:def 13;

set g = [#] (f,(the_unity_wrt multcomplex));

defpred S

A11: for k being Nat st S

S

proof

Seg 0 = {}. NAT
;
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

A12: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is integer_{1}[k]
; :: thesis: S_{1}[k + 1]

then reconsider a = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1), b = multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex)))) as Integer by A12;

not k + 1 in Seg k by FINSEQ_3:8;

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:2

.= b * a by BINOP_2:def 5 ;

hence S_{1}[k + 1]
by FINSEQ_1:9; :: thesis: verum

end;A12: ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is integer

proof
end;

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

end;

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:20;

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

end;hence ([#] (f,(the_unity_wrt multcomplex))) . (k + 1) is integer by A9; :: thesis: verum

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:20; :: thesis: verum

end;then reconsider a = ([#] (f,(the_unity_wrt multcomplex))) . (k + 1), b = multcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt multcomplex)))) as Integer by A12;

not k + 1 in Seg k by FINSEQ_3:8;

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:2

.= b * a by BINOP_2:def 5 ;

hence S

then A13: S

A14: for n being Nat holds S

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;

thus Product F is integer by A10, A16, A15, A14; :: thesis: verum