let f1, f2 be PartFunc of REAL , REAL ; :: thesis: ( f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) implies ( f1 (#) f2 is convergent_in+infty & lim_in+infty (f1 (#) f2) = (lim_in+infty f1) * (lim_in+infty f2) ) )
assume A1: ( f1 is convergent_in+infty & f2 is convergent_in+infty & ( for r being Real ex g being Real st
( r < g & g in dom (f1 (#) f2) ) ) ) ; :: thesis: ( f1 (#) f2 is convergent_in+infty & lim_in+infty (f1 (#) f2) = (lim_in+infty f1) * (lim_in+infty f2) )

A2: now

let seq be Real_Sequence; :: thesis: ( seq is divergent_to+infty & rng seq c= dom (f1 (#) f2) implies ( (f1 (#) f2) /* seq is convergent & lim ((f1 (#) f2) /* seq) = (lim_in+infty f1) * (lim_in+infty f2) ) )
A3: ( lim_in+infty f1 = lim_in+infty f1 & lim_in+infty f2 = lim_in+infty f2 ) ;
assume A4: ( seq is divergent_to+infty & rng seq c= dom (f1 (#) f2) ) ; :: thesis: ( (f1 (#) f2) /* seq is convergent & lim ((f1 (#) f2) /* seq) = (lim_in+infty f1) * (lim_in+infty f2) )
then A5: ( dom (f1 (#) f2) = (dom f1) /\ (dom f2) & rng seq c= dom f1 & rng seq c= dom f2 ) by Lm3;
then A6: ( f1 /* seq is convergent & lim (f1 /* seq) = lim_in+infty f1 ) by A1, A3, A4, Def12;
A7: ( f2 /* seq is convergent & lim (f2 /* seq) = lim_in+infty f2 ) by A1, A3, A4, A5, Def12;
then (f1 /* seq) (#) (f2 /* seq) is convergent by A6, SEQ_2:28;
hence (f1 (#) f2) /* seq is convergent by A4, A5, RFUNCT_2:23; :: thesis: lim ((f1 (#) f2) /* seq) = (lim_in+infty f1) * (lim_in+infty f2)
thus lim ((f1 (#) f2) /* seq) = lim ((f1 /* seq) (#) (f2 /* seq)) by A4, A5, RFUNCT_2:23
.= (lim_in+infty f1) * (lim_in+infty f2) by A6, A7, SEQ_2:29 ; :: thesis: verum

end;

hence f1 (#) f2 is convergent_in+infty by A1, Def6; :: thesis: lim_in+infty (f1 (#) f2) = (lim_in+infty f1) * (lim_in+infty f2)
hence lim_in+infty (f1 (#) f2) = (lim_in+infty f1) * (lim_in+infty f2) by A2, Def12; :: thesis: verum