let I be FinSequence of INT ; :: thesis: Sum I = addint $$ I
set g = addint ;
set h = addcomplex ;
set i = [#] (I,(the_unity_wrt addint));
rng I c= COMPLEX by NUMBERS:11;
then reconsider f = I as FinSequence of COMPLEX by FINSEQ_1:def 4;
set j = [#] (f,(the_unity_wrt addcomplex));
consider n being Nat such that
A1: dom f = Seg n by FINSEQ_1:def 2;
A2: ( addint $$ I = addint $$ ((finSeg n),([#] (I,(the_unity_wrt addint)))) & addcomplex $$ f = addcomplex $$ ((finSeg n),([#] (f,(the_unity_wrt addcomplex)))) ) by A1, SETWOP_2:def 2;
defpred S₁[ Nat] means addint $$ ((finSeg $1),([#] (I,(the_unity_wrt addint)))) = addcomplex $$ ((finSeg $1),([#] (f,(the_unity_wrt addcomplex))));
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
set b = addint $$ ((finSeg k),([#] (I,(the_unity_wrt addint))));
set a = ([#] (I,(the_unity_wrt addint))) . (k + 1);
A5: not k + 1 in Seg k by FINSEQ_3:8;
addint $$ ((finSeg (k + 1)),([#] (I,(the_unity_wrt addint)))) = addint $$ (((finSeg k) \/ {.(k + 1).}),([#] (I,(the_unity_wrt addint)))) by FINSEQ_1:9
.= addint . ((addint $$ ((finSeg k),([#] (I,(the_unity_wrt addint))))),(([#] (I,(the_unity_wrt addint))) . (k + 1))) by A5, SETWOP_2:2
.= (addint $$ ((finSeg k),([#] (I,(the_unity_wrt addint))))) + (([#] (I,(the_unity_wrt addint))) . (k + 1)) by BINOP_2:def 20
.= addcomplex . ((addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex))))),(([#] (f,(the_unity_wrt addcomplex))) . (k + 1))) by A4, BINOP_2:1, BINOP_2:4, BINOP_2:def 3
.= addcomplex $$ (((finSeg k) \/ {.(k + 1).}),([#] (f,(the_unity_wrt addcomplex)))) by A5, SETWOP_2:2
.= addcomplex $$ ((finSeg (k + 1)),([#] (f,(the_unity_wrt addcomplex)))) by FINSEQ_1:9 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A6: Seg 0 = {}. NAT ;
then addint $$ ((finSeg 0),([#] (I,(the_unity_wrt addint)))) = the_unity_wrt addcomplex by BINOP_2:1, BINOP_2:4, SETWISEO:31
.= addcomplex $$ ((finSeg 0),([#] (f,(the_unity_wrt addcomplex)))) by A6, SETWISEO:31 ;
then A7: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A7, A3);
then addint $$ I = addcomplex $$ f by A2;
hence Sum I = addint $$ I by RVSUM_1:def 10; :: thesis: verum