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

A2: now

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

end;

now

let seq be Real_Sequence; :: thesis:
assume A4: ( seq is divergent_to+infty & rng seq c= dom (f1 + f2) ) ; :: thesis:
then A5: ( dom (f1 + f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 ) by Lm2;
then A6: f1 /* seq is divergent_to-infty by A1, A4, Def8;
f2 /* seq is divergent_to-infty by A1, A4, A5, Def8;
then (f1 /* seq) + (f2 /* seq) is divergent_to-infty by A6, Th38;
hence (f1 + f2) /* seq is divergent_to-infty by A4, A5, RFUNCT_2:23; :: thesis:

end;

hence f1 + f2 is divergent_in+infty_to-infty by A2, Def8; :: thesis:

A7: now

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

end;

now

let seq be Real_Sequence; :: thesis:
assume A9: ( seq is divergent_to+infty & rng seq c= dom (f1 (#) f2) ) ; :: thesis:
then A10: ( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 ) by Lm3;
then A11: f1 /* seq is divergent_to-infty by A1, A9, Def8;
f2 /* seq is divergent_to-infty by A1, A9, A10, Def8;
then (f1 /* seq) (#) (f2 /* seq) is divergent_to+infty by A11, Th51;
hence (f1 (#) f2) /* seq is divergent_to+infty by A9, A10, RFUNCT_2:23; :: thesis:

end;

hence f1 (#) f2 is divergent_in+infty_to+infty by A7, Def7; :: thesis: