let I be FinSequence of INT ; :: thesis: Sum I = addint $$ I
rng I c= COMPLEX
by NUMBERS:11, XBOOLE_1:1;
then reconsider f = I as FinSequence of COMPLEX by FINSEQ_1:def 4;
set g = addint ;
set h = addcomplex ;
consider n being Nat such that
A1:
dom f = Seg n
by FINSEQ_1:def 2;
set i = [#] I,(the_unity_wrt addint );
set j = [#] f,(the_unity_wrt addcomplex );
A2:
addint $$ I = addint $$ (finSeg n),([#] I,(the_unity_wrt addint ))
by A1, SETWOP_2:def 2;
A3:
addcomplex $$ f = addcomplex $$ (finSeg n),([#] f,(the_unity_wrt addcomplex ))
by A1, SETWOP_2:def 2;
defpred S1[ Nat] means addint $$ (finSeg $1),([#] I,(the_unity_wrt addint )) = addcomplex $$ (finSeg $1),([#] f,(the_unity_wrt addcomplex ));
A4:
Seg 0 = {}. NAT
;
A5:
S1[ 0 ]
A6:
for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be
Nat;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A7:
S1[
k]
;
:: thesis: S1[k + 1]
set a =
([#] I,(the_unity_wrt addint )) . (k + 1);
set b =
addint $$ (finSeg k),
([#] I,(the_unity_wrt addint ));
A8:
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 A8, 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 A7, BINOP_2:1, BINOP_2:4, BINOP_2:def 3
.=
addcomplex $$ ((finSeg k) \/ {.(k + 1).}),
([#] f,(the_unity_wrt addcomplex ))
by A8, SETWOP_2:4
.=
addcomplex $$ (finSeg (k + 1)),
([#] f,(the_unity_wrt addcomplex ))
by FINSEQ_1:11
;
hence
S1[
k + 1]
;
:: thesis: verum
end;
for k being Nat holds S1[k]
from NAT_1:sch 2(A5, A6);
then
addint $$ I = addcomplex $$ f
by A2, A3;
hence
Sum I = addint $$ I
by RVSUM_1:def 11; :: thesis: verum