let x0 be Real; :: thesis: 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; :: thesis: ( 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) ) ; :: thesis: ( f1 + f2 is_divergent_to-infty_in x0 & f1 (#) f2 is_divergent_to+infty_in x0 )

A4: now :: thesis: 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; :: thesis: ( 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} ; :: thesis: (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; :: thesis: verum

end;

A11: now :: thesis: 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; :: thesis: ( 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} ; :: thesis: (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; :: thesis: verum

end;

now :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: verum

end;

hence f1 + f2 is_divergent_to-infty_in x0 by A4; :: thesis: f1 (#) f2 is_divergent_to+infty_in x0

now :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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; :: thesis: verum

end;

hence f1 (#) f2 is_divergent_to+infty_in x0 by A11; :: thesis: verum