let x0 be Real; :: thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f2,x0) <> 0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 / f2) ) ) holds
( f1 / f2 is_left_convergent_in x0 & lim_left ((f1 / f2),x0) = (lim_left (f1,x0)) / (lim_left (f2,x0)) )
let f1, f2 be PartFunc of REAL,REAL; :: thesis: ( f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left (f2,x0) <> 0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 / f2) ) ) implies ( f1 / f2 is_left_convergent_in x0 & lim_left ((f1 / f2),x0) = (lim_left (f1,x0)) / (lim_left (f2,x0)) ) )
assume that
A1: f1 is_left_convergent_in x0 and
A2: f2 is_left_convergent_in x0 and
A3: lim_left (f2,x0) <> 0 and
A4: for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 / f2) ) ; :: thesis: ( f1 / f2 is_left_convergent_in x0 & lim_left ((f1 / f2),x0) = (lim_left (f1,x0)) / (lim_left (f2,x0)) )

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

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

end;

then A11: f2 ^ is_left_convergent_in x0 by A2, A3, Th49;
A12: f1 / f2 = f1 (#) (f2 ^) by RFUNCT_1:31;
hence f1 / f2 is_left_convergent_in x0 by A1, A4, A11, Th50; :: thesis: lim_left ((f1 / f2),x0) = (lim_left (f1,x0)) / (lim_left (f2,x0))
lim_left ((f2 ^),x0) = (lim_left (f2,x0)) " by A2, A3, A5, Th49;
hence lim_left ((f1 / f2),x0) = (lim_left (f1,x0)) * ((lim_left (f2,x0)) ") by A1, A4, A12, A11, Th50
.= (lim_left (f1,x0)) / (lim_left (f2,x0)) by XCMPLX_0:def 9 ;
:: thesis: verum