let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st f1 is_divergent_to-infty_in x0 & f2 is_divergent_to-infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in (dom f1) /\ (dom f2) & g2 < r2 & x0 < g2 & g2 in (dom f1) /\ (dom f2) ) ) holds
( f1 + f2 is_divergent_to-infty_in x0 & f1 (#) f2 is_divergent_to+infty_in x0 )
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_divergent_to-infty_in x0 & f2 is_divergent_to-infty_in x0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in (dom f1) /\ (dom f2) & g2 < r2 & x0 < g2 & g2 in (dom f1) /\ (dom f2) ) ) implies ( f1 + f2 is_divergent_to-infty_in x0 & f1 (#) f2 is_divergent_to+infty_in x0 ) )
assume that
A1:
f1 is_divergent_to-infty_in x0
and
A2:
f2 is_divergent_to-infty_in x0
and
A3:
for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in (dom f1) /\ (dom f2) & g2 < r2 & x0 < g2 & g2 in (dom f1) /\ (dom f2) )
; ( f1 + f2 is_divergent_to-infty_in x0 & f1 (#) f2 is_divergent_to+infty_in x0 )
A4:
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom (f1 + f2)) \ {x0} holds
(f1 + f2) /* s is divergent_to-infty let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom (f1 + f2)) \ {x0} implies (f1 + f2) /* s is divergent_to-infty )assume that A5:
s is
convergent
and A6:
lim s = x0
and A7:
rng s c= (dom (f1 + f2)) \ {x0}
;
(f1 + f2) /* s is divergent_to-infty
rng s c= (dom f2) \ {x0}
by A7, Lm4;
then A8:
f2 /* s is
divergent_to-infty
by A2, A5, A6;
rng s c= (dom f1) \ {x0}
by A7, Lm4;
then
f1 /* s is
divergent_to-infty
by A1, A5, A6;
then A9:
(f1 /* s) + (f2 /* s) is
divergent_to-infty
by A8, LIMFUNC1:11;
A10:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by A7, Lm4;
rng s c= dom (f1 + f2)
by A7, Lm4;
hence
(f1 + f2) /* s is
divergent_to-infty
by A10, A9, RFUNCT_2:8;
verum end;
A11:
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) \ {x0} holds
(f1 (#) f2) /* s is divergent_to+infty let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom (f1 (#) f2)) \ {x0} implies (f1 (#) f2) /* s is divergent_to+infty )assume that A12:
s is
convergent
and A13:
lim s = x0
and A14:
rng s c= (dom (f1 (#) f2)) \ {x0}
;
(f1 (#) f2) /* s is divergent_to+infty
rng s c= (dom f2) \ {x0}
by A14, Lm2;
then A15:
f2 /* s is
divergent_to-infty
by A2, A12, A13;
rng s c= (dom f1) \ {x0}
by A14, Lm2;
then
f1 /* s is
divergent_to-infty
by A1, A12, A13;
then A16:
(f1 /* s) (#) (f2 /* s) is
divergent_to+infty
by A15, LIMFUNC1:24;
A17:
dom (f1 (#) f2) = (dom f1) /\ (dom f2)
by A14, Lm2;
rng s c= dom (f1 (#) f2)
by A14, Lm2;
hence
(f1 (#) f2) /* s is
divergent_to+infty
by A17, A16, RFUNCT_2:8;
verum end;
now for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) )let r1,
r2 be
Real;
( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) ) )assume that A18:
r1 < x0
and A19:
x0 < r2
;
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) )consider g1,
g2 being
Real such that A20:
r1 < g1
and A21:
g1 < x0
and A22:
g1 in (dom f1) /\ (dom f2)
and A23:
g2 < r2
and A24:
x0 < g2
and A25:
g2 in (dom f1) /\ (dom f2)
by A3, A18, A19;
take g1 =
g1;
ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) )take g2 =
g2;
( r1 < g1 & g1 < x0 & g1 in dom (f1 + f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 + f2) )thus
(
r1 < g1 &
g1 < x0 &
g1 in dom (f1 + f2) &
g2 < r2 &
x0 < g2 &
g2 in dom (f1 + f2) )
by A20, A21, A22, A23, A24, A25, VALUED_1:def 1;
verum end;
hence
f1 + f2 is_divergent_to-infty_in x0
by A4; f1 (#) f2 is_divergent_to+infty_in x0
now for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) )let r1,
r2 be
Real;
( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) ) )assume that A26:
r1 < x0
and A27:
x0 < r2
;
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) )consider g1,
g2 being
Real such that A28:
r1 < g1
and A29:
g1 < x0
and A30:
g1 in (dom f1) /\ (dom f2)
and A31:
g2 < r2
and A32:
x0 < g2
and A33:
g2 in (dom f1) /\ (dom f2)
by A3, A26, A27;
take g1 =
g1;
ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) )take g2 =
g2;
( r1 < g1 & g1 < x0 & g1 in dom (f1 (#) f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 (#) f2) )thus
(
r1 < g1 &
g1 < x0 &
g1 in dom (f1 (#) f2) &
g2 < r2 &
x0 < g2 &
g2 in dom (f1 (#) f2) )
by A28, A29, A30, A31, A32, A33, VALUED_1:def 4;
verum end;
hence
f1 (#) f2 is_divergent_to+infty_in x0
by A11; verum