let f1, f2 be PartFunc of REAL,REAL; :: thesis:
assume that
A1: f1 is convergent_in+infty and
A2: f2 is convergent_in+infty and
A3: for r being Real ex g being Real st
( r < g & g in dom (f1 (#) 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, Lm3;
A8: rng seq c= dom f2 by A6, Lm3;
then A9: lim (f2 /* seq) = lim_in+infty f2 by A2, A5, Def12;
A10: f2 /* seq is convergent by A2, A5, A8;
A11: rng seq c= dom f1 by A6, Lm3;
then A12: lim (f1 /* seq) = lim_in+infty f1 by A1, A5, Def12;
A13: f1 /* seq is convergent by A1, A5, A11;
then (f1 /* seq) (#) (f2 /* seq) is convergent by A10;
hence (f1 (#) f2) /* seq is convergent by A6, A7, RFUNCT_2:8; :: thesis:
thus lim ((f1 (#) f2) /* seq) = lim ((f1 /* seq) (#) (f2 /* seq)) by A6, A7, RFUNCT_2:8
.= (lim_in+infty f1) * (lim_in+infty f2) by A13, A12, A10, A9, SEQ_2:15 ; :: thesis:

end;

hence f1 (#) f2 is convergent_in+infty by A3; :: thesis:
hence lim_in+infty (f1 (#) f2) = (lim_in+infty f1) * (lim_in+infty f2) by A4, Def12; :: thesis: