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
( g < r & 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
( g < r & 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) )
A5: ( (dom f1) /\ (dom f2) c= dom f1 & (dom f1) /\ (dom f2) c= dom f2 ) by XBOOLE_1:17;
A6: dom (f1 (#) f2) = (dom f1) /\ (dom f2) by VALUED_1:def 4;
then rng seq c= dom f1 by A4, A5, XBOOLE_1:1;
then A7: ( f1 /* seq is convergent & lim (f1 /* seq) = lim_in-infty f1 ) by A1, A3, A4, Def13;
rng seq c= dom f2 by A4, A5, A6, XBOOLE_1:1;
then A8: ( f2 /* seq is convergent & lim (f2 /* seq) = lim_in-infty f2 ) by A1, A3, A4, Def13;
then (f1 /* seq) (#) (f2 /* seq) is convergent by A7, SEQ_2:28;
hence (f1 (#) f2) /* seq is convergent by A4, A6, 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, A6, RFUNCT_2:23
.= (lim_in-infty f1) * (lim_in-infty f2) by A7, A8, SEQ_2:29 ; :: thesis: verum

end;

hence f1 (#) f2 is convergent_in-infty by A1, Def9; :: 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, Def13; :: thesis: verum