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,(the_unity_wrt addcomplex));
defpred S₁[ Nat] means addcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt addcomplex)))) is integer ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
A4: ([#] (f,(the_unity_wrt addcomplex))) . (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 addcomplex))) . (k + 1) is integer

then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = f . (k + 1) by SETWOP_2:20;
hence ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is integer by A1; :: thesis: verum

end;

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

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

end;

end;

end;

assume S₁[k] ; :: thesis: S₁[k + 1]
then reconsider a = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1), b = addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex)))) as Integer by A4;
not k + 1 in Seg k by FINSEQ_3:8;
then addcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt addcomplex)))) = addcomplex . ((addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex))))),(([#] (f,(the_unity_wrt addcomplex))) . (k + 1))) by SETWOP_2:2
.= b + a by BINOP_2:def 3 ;
hence S₁[k + 1] by FINSEQ_1:9; :: thesis: verum

end;

Seg 0 = {}. NAT ;
then A5: S₁[ 0 ] by BINOP_2:1, SETWISEO:31;
A6: for n being Nat holds S₁[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 $$ ((findom f),([#] (f,(the_unity_wrt addcomplex)))) by SETWOP_2:def 2;
thus Sum F is integer by A2, A8, A7, A6; :: thesis: verum