let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f2 <> 0 & ( 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 that
A1: f1 is convergent_in+infty and
A2: ( f2 is convergent_in+infty & lim_in+infty f2 <> 0 ) and
A3: 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) )
dom (f1 / f2) = (dom f1) /\ ((dom f2) \ (f2 " {0})) by RFUNCT_1:def 1;
then A4: dom (f1 / f2) = (dom f1) /\ (dom (f2 ^)) by RFUNCT_1:def 2;
A5: (dom f1) /\ (dom (f2 ^)) c= dom (f2 ^) by XBOOLE_1:17;

A6: now :: thesis: for r being Real ex g being Real st
( r < g & g in dom f2 & f2 . g <> 0 )

let r be Real; :: thesis: ex g being Real st
( r < g & g in dom f2 & f2 . g <> 0 )
consider g being Real such that
A7: r < g and
A8: g in dom (f1 / f2) by A3;
take g = g; :: thesis: ( r < g & g in dom f2 & f2 . g <> 0 )
g in dom (f2 ^) by A4, A5, A8;
then A9: g in (dom f2) \ (f2 " {0}) by RFUNCT_1:def 2;
then ( g in dom f2 & not g in f2 " {0} ) by XBOOLE_0:def 5;
then not f2 . g in {0} by FUNCT_1:def 7;
hence ( r < g & g in dom f2 & f2 . g <> 0 ) by A7, A9, TARSKI:def 1, XBOOLE_0:def 5; :: thesis: verum

end;

then A10: f2 ^ is convergent_in+infty by A2, Th86;
A11: lim_in+infty (f2 ^) = (lim_in+infty f2) " by A2, A6, Th86;

A12: now :: thesis: for r being Real ex g being Real st
( r < g & g in dom (f1 (#) (f2 ^)) )

let r be Real; :: thesis: ex g being Real st
( r < g & g in dom (f1 (#) (f2 ^)) )
consider g being Real such that
A13: ( r < g & g in dom (f1 / f2) ) by A3;
take g = g; :: thesis: ( r < g & g in dom (f1 (#) (f2 ^)) )
thus ( r < g & g in dom (f1 (#) (f2 ^)) ) by A4, A13, VALUED_1:def 4; :: thesis: verum

end;

then f1 (#) (f2 ^) is convergent_in+infty by A1, A10, Th87;
hence f1 / f2 is convergent_in+infty by RFUNCT_1:31; :: thesis: lim_in+infty (f1 / f2) = (lim_in+infty f1) / (lim_in+infty f2)
thus lim_in+infty (f1 / f2) = lim_in+infty (f1 (#) (f2 ^)) by RFUNCT_1:31
.= (lim_in+infty f1) * ((lim_in+infty f2) ") by A1, A12, A10, A11, Th87
.= (lim_in+infty f1) / (lim_in+infty f2) by XCMPLX_0:def 9 ; :: thesis: verum