let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim (f2,x0) <> 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 / f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 / f2) ) ) holds
( f1 / f2 is_convergent_in x0 & lim ((f1 / f2),x0) = (lim (f1,x0)) / (lim (f2,x0)) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim (f2,x0) <> 0 & ( for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 / f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 / f2) ) ) implies ( f1 / f2 is_convergent_in x0 & lim ((f1 / f2),x0) = (lim (f1,x0)) / (lim (f2,x0)) ) )
assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in x0 and
A3: lim (f2,x0) <> 0 and
A4: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f1 / f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 / f2) ) ; :: thesis: ( f1 / f2 is_convergent_in x0 & lim ((f1 / f2),x0) = (lim (f1,x0)) / (lim (f2,x0)) )

A5: now :: thesis: for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f2 & g2 < r2 & x0 < g2 & g2 in dom f2 & f2 . g1 <> 0 & f2 . g2 <> 0 )

let r1, r2 be Real; :: thesis: ( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f2 & g2 < r2 & x0 < g2 & g2 in dom f2 & f2 . g1 <> 0 & f2 . g2 <> 0 ) )
assume that
A6: r1 < x0 and
A7: x0 < r2 ; :: thesis: ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f2 & g2 < r2 & x0 < g2 & g2 in dom f2 & f2 . g1 <> 0 & f2 . g2 <> 0 )
consider g1, g2 being Real such that
A8: r1 < g1 and
A9: g1 < x0 and
A10: g1 in dom (f1 / f2) and
A11: g2 < r2 and
A12: x0 < g2 and
A13: g2 in dom (f1 / f2) by A4, A6, A7;
take g1 = g1; :: thesis: ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f2 & g2 < r2 & x0 < g2 & g2 in dom f2 & f2 . g1 <> 0 & f2 . g2 <> 0 )
take g2 = g2; :: thesis: ( r1 < g1 & g1 < x0 & g1 in dom f2 & g2 < r2 & x0 < g2 & g2 in dom f2 & f2 . g1 <> 0 & f2 . g2 <> 0 )
thus ( r1 < g1 & g1 < x0 ) by A8, A9; :: thesis: ( g1 in dom f2 & g2 < r2 & x0 < g2 & g2 in dom f2 & f2 . g1 <> 0 & f2 . g2 <> 0 )
A14: dom (f1 / f2) = (dom f1) /\ ((dom f2) \ (f2 " {0})) by RFUNCT_1:def 1;
then g2 in (dom f2) \ (f2 " {0}) by A13, XBOOLE_0:def 4;
then not g2 in f2 " {0} by XBOOLE_0:def 5;
then A15: not f2 . g2 in {0} by A13, A14, FUNCT_1:def 7;
g1 in (dom f2) \ (f2 " {0}) by A10, A14, XBOOLE_0:def 4;
then not g1 in f2 " {0} by XBOOLE_0:def 5;
then not f2 . g1 in {0} by A10, A14, FUNCT_1:def 7;
hence ( g1 in dom f2 & g2 < r2 & x0 < g2 & g2 in dom f2 & f2 . g1 <> 0 & f2 . g2 <> 0 ) by A10, A11, A12, A13, A14, A15, TARSKI:def 1; :: thesis: verum

end;

then A16: f2 ^ is_convergent_in x0 by A2, A3, Th37;
A17: f1 / f2 = f1 (#) (f2 ^) by RFUNCT_1:31;
hence f1 / f2 is_convergent_in x0 by A1, A4, A16, Th38; :: thesis: lim ((f1 / f2),x0) = (lim (f1,x0)) / (lim (f2,x0))
lim ((f2 ^),x0) = (lim (f2,x0)) " by A2, A3, A5, Th37;
hence lim ((f1 / f2),x0) = (lim (f1,x0)) * ((lim (f2,x0)) ") by A1, A4, A17, A16, Th38
.= (lim (f1,x0)) / (lim (f2,x0)) by XCMPLX_0:def 9 ;
:: thesis: verum