let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st f1 is_right_divergent_to-infty_in x0 & f2 is_right_divergent_to-infty_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is_right_divergent_to-infty_in x0 & f1 (#) f2 is_right_divergent_to+infty_in x0 )
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_right_divergent_to-infty_in x0 & f2 is_right_divergent_to-infty_in x0 & ( for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in (dom f1) /\ (dom f2) ) ) implies ( f1 + f2 is_right_divergent_to-infty_in x0 & f1 (#) f2 is_right_divergent_to+infty_in x0 ) )
assume that
A1:
f1 is_right_divergent_to-infty_in x0
and
A2:
f2 is_right_divergent_to-infty_in x0
and
A3:
for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in (dom f1) /\ (dom f2) )
; ( f1 + f2 is_right_divergent_to-infty_in x0 & f1 (#) f2 is_right_divergent_to+infty_in x0 )
A4:
now for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (f1 + f2)) /\ (right_open_halfline x0) holds
(f1 + f2) /* seq is divergent_to-infty let seq be
Real_Sequence;
( seq is convergent & lim seq = x0 & rng seq c= (dom (f1 + f2)) /\ (right_open_halfline x0) implies (f1 + f2) /* seq is divergent_to-infty )assume that A5:
seq is
convergent
and A6:
lim seq = x0
and A7:
rng seq c= (dom (f1 + f2)) /\ (right_open_halfline x0)
;
(f1 + f2) /* seq is divergent_to-infty
rng seq c= (dom f2) /\ (right_open_halfline x0)
by A7, Lm4;
then A8:
f2 /* seq is
divergent_to-infty
by A2, A5, A6;
rng seq c= (dom f1) /\ (right_open_halfline x0)
by A7, Lm4;
then
f1 /* seq is
divergent_to-infty
by A1, A5, A6;
then A9:
(f1 /* seq) + (f2 /* seq) is
divergent_to-infty
by A8, LIMFUNC1:11;
A10:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by A7, Lm4;
rng seq c= dom (f1 + f2)
by A7, Lm4;
hence
(f1 + f2) /* seq is
divergent_to-infty
by A10, A9, RFUNCT_2:8;
verum end;
A11:
now for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (f1 (#) f2)) /\ (right_open_halfline x0) holds
(f1 (#) f2) /* seq is divergent_to+infty let seq be
Real_Sequence;
( seq is convergent & lim seq = x0 & rng seq c= (dom (f1 (#) f2)) /\ (right_open_halfline x0) implies (f1 (#) f2) /* seq is divergent_to+infty )assume that A12:
seq is
convergent
and A13:
lim seq = x0
and A14:
rng seq c= (dom (f1 (#) f2)) /\ (right_open_halfline x0)
;
(f1 (#) f2) /* seq is divergent_to+infty
rng seq c= (dom f2) /\ (right_open_halfline x0)
by A14, Lm2;
then A15:
f2 /* seq is
divergent_to-infty
by A2, A12, A13;
rng seq c= (dom f1) /\ (right_open_halfline x0)
by A14, Lm2;
then
f1 /* seq is
divergent_to-infty
by A1, A12, A13;
then A16:
(f1 /* seq) (#) (f2 /* seq) is
divergent_to+infty
by A15, LIMFUNC1:24;
A17:
dom (f1 (#) f2) = (dom f1) /\ (dom f2)
by A14, Lm2;
rng seq c= dom (f1 (#) f2)
by A14, Lm2;
hence
(f1 (#) f2) /* seq is
divergent_to+infty
by A17, A16, RFUNCT_2:8;
verum end;
hence
f1 + f2 is_right_divergent_to-infty_in x0
by A4; f1 (#) f2 is_right_divergent_to+infty_in x0
hence
f1 (#) f2 is_right_divergent_to+infty_in x0
by A11; verum