let f1, f2 be PartFunc of REAL,REAL; ( f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 + f2) ) ) implies ( f1 + f2 is convergent_in+infty & lim_in+infty (f1 + f2) = (lim_in+infty f1) + (lim_in+infty f2) ) )
assume that
A1:
f1 is convergent_in+infty
and
A2:
f2 is convergent_in+infty
and
A3:
for r being Real ex g being Real st
( r < g & g in dom (f1 + f2) )
; ( f1 + f2 is convergent_in+infty & lim_in+infty (f1 + f2) = (lim_in+infty f1) + (lim_in+infty f2) )
A4:
now for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom (f1 + f2) holds
( (f1 + f2) /* seq is convergent & lim ((f1 + f2) /* seq) = (lim_in+infty f1) + (lim_in+infty f2) )let seq be
Real_Sequence;
( seq is divergent_to+infty & rng seq c= dom (f1 + f2) implies ( (f1 + f2) /* seq is convergent & lim ((f1 + f2) /* seq) = (lim_in+infty f1) + (lim_in+infty f2) ) )assume that A5:
seq is
divergent_to+infty
and A6:
rng seq c= dom (f1 + f2)
;
( (f1 + f2) /* seq is convergent & lim ((f1 + f2) /* seq) = (lim_in+infty f1) + (lim_in+infty f2) )A7:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by A6, Lm2;
A8:
rng seq c= dom f2
by A6, Lm2;
then A9:
lim (f2 /* seq) = lim_in+infty f2
by A2, A5, Def12;
A10:
f2 /* seq is
convergent
by A2, A5, A8;
A11:
rng seq c= dom f1
by A6, Lm2;
then A12:
lim (f1 /* seq) = lim_in+infty f1
by A1, A5, Def12;
A13:
f1 /* seq is
convergent
by A1, A5, A11;
then
(f1 /* seq) + (f2 /* seq) is
convergent
by A10;
hence
(f1 + f2) /* seq is
convergent
by A6, A7, RFUNCT_2:8;
lim ((f1 + f2) /* seq) = (lim_in+infty f1) + (lim_in+infty f2)thus lim ((f1 + f2) /* seq) =
lim ((f1 /* seq) + (f2 /* seq))
by A6, A7, RFUNCT_2:8
.=
(lim_in+infty f1) + (lim_in+infty f2)
by A13, A12, A10, A9, SEQ_2:6
;
verum end;
hence
f1 + f2 is convergent_in+infty
by A3; lim_in+infty (f1 + f2) = (lim_in+infty f1) + (lim_in+infty f2)
hence
lim_in+infty (f1 + f2) = (lim_in+infty f1) + (lim_in+infty f2)
by A4, Def12; verum