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,);
defpred S1[ Nat] means multcomplex \$\$ ((),([#] (f,))) is integer ;
A11: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A12: ([#] (f,)) . (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,)) . (k + 1) is integer
then ([#] (f,)) . (k + 1) = f . (k + 1) by SETWOP_2:20;
hence ([#] (f,)) . (k + 1) is integer by A9; :: thesis: verum
end;
suppose not k + 1 in dom f ; :: thesis: ([#] (f,)) . (k + 1) is integer
hence ([#] (f,)) . (k + 1) is integer by ; :: thesis: verum
end;
end;
end;
assume S1[k] ; :: thesis: S1[k + 1]
then reconsider a = ([#] (f,)) . (k + 1), b = multcomplex \$\$ ((),([#] (f,))) as Integer by A12;
not k + 1 in Seg k by FINSEQ_3:8;
then multcomplex \$\$ ((() \/ {.(k + 1).}),([#] (f,))) = multcomplex . ((multcomplex \$\$ ((),([#] (f,)))),(([#] (f,)) . (k + 1))) by SETWOP_2:2
.= b * a by BINOP_2:def 5 ;
hence S1[k + 1] by FINSEQ_1:9; :: thesis: verum
end;
Seg 0 = {}. NAT ;
then A13: S1[ 0 ] by ;
A14: for n being Nat holds S1[n] from consider n being Nat such that
A15: dom f = Seg n by FINSEQ_1:def 2;
A16: multcomplex \$\$ f = multcomplex \$\$ ((),([#] (f,))) by SETWOP_2:def 2;
thus Product F is integer by A10, A16, A15, A14; :: thesis: verum