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

A4: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A5: seq is divergent_to+infty and
A6: rng seq c= dom (f1 + f2) ; :: thesis:
A7: dom (f1 + f2) = (dom f1) /\ (dom f2) by A6, Lm2;
rng seq c= dom f2 by A6, Lm2;
then A8: f2 /* seq is divergent_to+infty by A2, A5;
rng seq c= dom f1 by A6, Lm2;
then f1 /* seq is divergent_to+infty by A1, A5;
then (f1 /* seq) + (f2 /* seq) is divergent_to+infty by A8, Th8;
hence (f1 + f2) /* seq is divergent_to+infty by A6, A7, RFUNCT_2:8; :: thesis:

end;

A9: now :: thesis:

let seq be Real_Sequence; :: thesis:
assume that
A10: seq is divergent_to+infty and
A11: rng seq c= dom (f1 (#) f2) ; :: thesis:
A12: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by A11, Lm3;
rng seq c= dom f2 by A11, Lm3;
then A13: f2 /* seq is divergent_to+infty by A2, A10;
rng seq c= dom f1 by A11, Lm3;
then f1 /* seq is divergent_to+infty by A1, A10;
then (f1 /* seq) (#) (f2 /* seq) is divergent_to+infty by A13, Th10;
hence (f1 (#) f2) /* seq is divergent_to+infty by A11, A12, RFUNCT_2:8; :: thesis:

end;

now :: thesis:

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

end;

hence f1 + f2 is divergent_in+infty_to+infty by A4; :: thesis:

now :: thesis:

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

end;

hence f1 (#) f2 is divergent_in+infty_to+infty by A9; :: thesis: