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

proof

set j = [#] (f,(the_unity_wrt addcomplex));
set i = [#] (F,(the_unity_wrt addreal));
let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A5: ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1)

proof

per cases ( k + 1 in dom f or not k + 1 in dom f ) ;

suppose A6: k + 1 in dom f ; :: thesis: ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1)

then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = F . (k + 1) by SETWOP_2:20
.= ([#] (F,(the_unity_wrt addreal))) . (k + 1) by A6, SETWOP_2:20 ;
hence ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) ; :: thesis: verum

end;

suppose A7: not k + 1 in dom f ; :: thesis: ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1)

then ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) = the_unity_wrt addcomplex by SETWOP_2:20
.= ([#] (F,(the_unity_wrt addreal))) . (k + 1) by A7, BINOP_2:1, BINOP_2:2, SETWOP_2:20 ;
hence ([#] (F,(the_unity_wrt addreal))) . (k + 1) = ([#] (f,(the_unity_wrt addcomplex))) . (k + 1) ; :: thesis: verum

end;

end;

end;

A8: not k + 1 in Seg k by FINSEQ_3:8;
addreal $$ ((finSeg (k + 1)),([#] (F,(the_unity_wrt addreal)))) = addreal $$ (((finSeg k) \/ {.(In ((k + 1),NAT)).}),([#] (F,(the_unity_wrt addreal)))) by FINSEQ_1:9
.= addreal . ((addreal $$ ((finSeg k),([#] (F,(the_unity_wrt addreal))))),(([#] (F,(the_unity_wrt addreal))) . (k + 1))) by A8, SETWOP_2:2
.= (addreal $$ ((finSeg k),([#] (F,(the_unity_wrt addreal))))) + (([#] (F,(the_unity_wrt addreal))) . (k + 1)) by BINOP_2:def 9
.= addcomplex . ((addcomplex $$ ((finSeg k),([#] (f,(the_unity_wrt addcomplex))))),(([#] (f,(the_unity_wrt addcomplex))) . (k + 1))) by A4, A5, BINOP_2:def 3
.= addcomplex $$ (((finSeg k) \/ {.(In ((k + 1),NAT)).}),([#] (f,(the_unity_wrt addcomplex)))) by A8, SETWOP_2:2
.= addcomplex $$ ((finSeg (k + 1)),([#] (f,(the_unity_wrt addcomplex)))) by FINSEQ_1:9 ;
hence S₁[k + 1] ; :: thesis: verum

end;

A9: Seg 0 = {}. NAT ;
then addreal $$ ((finSeg 0),([#] (F,(the_unity_wrt addreal)))) = the_unity_wrt addcomplex by BINOP_2:1, BINOP_2:2, SETWISEO:31
.= addcomplex $$ ((finSeg 0),([#] (f,(the_unity_wrt addcomplex)))) by A9, SETWISEO:31 ;
then A10: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A10, A3);
then addreal $$ F = addcomplex $$ f by A2;
hence Sum F = addreal $$ F by Def10; :: thesis: verum