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_{1}[ Nat] means addcomplex $$ ((finSeg F),([#] (f,(the_unity_wrt addcomplex)))) is integer ;

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

S_{1}[k + 1]

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

A6: for n being Nat holds S_{1}[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

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

A3: for k being Nat st S

S

proof

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

A4: ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is integer_{1}[k]
; :: thesis: S_{1}[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_{1}[k + 1]
by FINSEQ_1:9; :: thesis: verum

end;A4: ([#] (f,(the_unity_wrt addcomplex))) . (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 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;hence ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) is integer by A1; :: thesis: verum

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

then A5: S

A6: for n being Nat holds S

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