set mc = addcomplex ;
consider f being FinSequence of COMPLEX such that
A1: f = F and
A2: Sum F = addcomplex \$\$ f by RVSUM_1:def 10;
set g = [#] (f,);
defpred S1[ Nat] means addcomplex \$\$ ((),([#] (f,))) is integer ;
A3: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
A4: ([#] (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 A1; :: 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 = addcomplex \$\$ ((),([#] (f,))) as Integer by A4;
not k + 1 in Seg k by FINSEQ_3:8;
then addcomplex \$\$ ((() \/ {.(k + 1).}),([#] (f,))) = addcomplex . ((addcomplex \$\$ ((),([#] (f,)))),(([#] (f,)) . (k + 1))) by SETWOP_2:2
.= b + a by BINOP_2:def 3 ;
hence S1[k + 1] by FINSEQ_1:9; :: thesis: verum
end;
Seg 0 = {}. NAT ;
then A5: S1[ 0 ] by ;
A6: for n being Nat holds S1[n] from NAT_1:sch 2(A5, A3);
consider n being Nat such that
A7: dom f = Seg n by FINSEQ_1:def 2;
A8: addcomplex \$\$ f = addcomplex \$\$ ((),([#] (f,))) by SETWOP_2:def 2;
thus Sum F is integer by A2, A8, A7, A6; :: thesis: verum