let x0 be Real; :: thesis:
let f1, f2 be PartFunc of REAL,REAL; :: thesis:
assume that
A1: f1 is_left_divergent_to+infty_in x0 and
A2: f2 is_left_divergent_to+infty_in x0 and
A3: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in (dom f1) /\ (dom f2) ) ; :: thesis:

A4: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A5: seq is convergent and
A6: lim seq = x0 and
A7: rng seq c= (dom (f1 + f2)) /\ (left_open_halfline x0) ; :: thesis:
rng seq c= (dom f2) /\ (left_open_halfline x0) by A7, Lm4;
then A8: f2 /* seq is divergent_to+infty by A2, A5, A6;
rng seq c= (dom f1) /\ (left_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:8;
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; :: thesis:

end;

A11: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A12: seq is convergent and
A13: lim seq = x0 and
A14: rng seq c= (dom (f1 (#) f2)) /\ (left_open_halfline x0) ; :: thesis:
rng seq c= (dom f2) /\ (left_open_halfline x0) by A14, Lm2;
then A15: f2 /* seq is divergent_to+infty by A2, A12, A13;
rng seq c= (dom f1) /\ (left_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:10;
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; :: thesis:

end;

now :: thesis:

let r be Real; :: thesis:
assume r < x0 ; :: thesis:
then consider g being Real such that
A18: r < g and
A19: g < x0 and
A20: g in (dom f1) /\ (dom f2) by A3;
take g = g; :: thesis:
thus ( r < g & g < x0 & g in dom (f1 + f2) ) by A18, A19, A20, VALUED_1:def 1; :: thesis:

end;

hence f1 + f2 is_left_divergent_to+infty_in x0 by A4; :: thesis:

now :: thesis:

let r be Real; :: thesis:
assume r < x0 ; :: thesis:
then consider g being Real such that
A21: r < g and
A22: g < x0 and
A23: g in (dom f1) /\ (dom f2) by A3;
take g = g; :: thesis:
thus ( r < g & g < x0 & g in dom (f1 (#) f2) ) by A21, A22, A23, VALUED_1:def 4; :: thesis:

end;

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