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, XBOOLE_1:1;
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:9;
addint $$ (finSeg (k + 1)),([#] I,(the_unity_wrt addint )) = addint $$ ((finSeg k) \/ {.(k + 1).}),([#] I,(the_unity_wrt addint )) by FINSEQ_1:11
.= addint . (addint $$ (finSeg k),([#] I,(the_unity_wrt addint ))),(([#] I,(the_unity_wrt addint )) . (k + 1)) by A5, SETWOP_2:4
.= (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:4
.= addcomplex $$ (finSeg (k + 1)),([#] f,(the_unity_wrt addcomplex )) by FINSEQ_1:11 ;
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:40
.= addcomplex $$ (finSeg 0 ),([#] f,(the_unity_wrt addcomplex )) by A6, SETWISEO:40 ;
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 11; :: thesis: verum