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 A1: ( 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) ) ) ) ; :: thesis: ( f1 / f2 is_convergent_in x0 & lim (f1 / f2),x0 = (lim f1,x0) / (lim f2,x0) )
A2: f1 / f2 = f1 (#) (f2 ^ ) by RFUNCT_1:47;

now

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 ( r1 < x0 & 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 )
then consider g1, g2 being Real such that
A3: ( r1 < g1 & g1 < x0 & g1 in dom (f1 / f2) & g2 < r2 & x0 < g2 & g2 in dom (f1 / f2) ) by A1;
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 A3; :: thesis: ( g1 in dom f2 & g2 < r2 & x0 < g2 & g2 in dom f2 & f2 . g1 <> 0 & f2 . g2 <> 0 )
A4: dom (f1 / f2) = (dom f1) /\ ((dom f2) \ (f2 " {0 })) by RFUNCT_1:def 4;
then ( g1 in (dom f2) \ (f2 " {0 }) & g2 in (dom f2) \ (f2 " {0 }) ) by A3, XBOOLE_0:def 4;
then ( g1 in dom f2 & not g1 in f2 " {0 } & g2 in dom f2 & not g2 in f2 " {0 } ) by XBOOLE_0:def 5;
then ( not f2 . g1 in {0 } & not f2 . g2 in {0 } ) by FUNCT_1:def 13;
hence ( g1 in dom f2 & g2 < r2 & x0 < g2 & g2 in dom f2 & f2 . g1 <> 0 & f2 . g2 <> 0 ) by A3, A4, TARSKI:def 1; :: thesis: verum

end;

then A5: ( f2 ^ is_convergent_in x0 & lim (f2 ^ ),x0 = (lim f2,x0) " ) by A1, Th41;
hence f1 / f2 is_convergent_in x0 by A1, A2, Th42; :: thesis: lim (f1 / f2),x0 = (lim f1,x0) / (lim f2,x0)
thus lim (f1 / f2),x0 = (lim f1,x0) * ((lim f2,x0) " ) by A1, A2, A5, Th42
.= (lim f1,x0) / (lim f2,x0) by XCMPLX_0:def 9 ; :: thesis: verum