let x0 be Real; 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; ( 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) )
; ( f1 / f2 is_convergent_in x0 & lim ((f1 / f2),x0) = (lim (f1,x0)) / (lim (f2,x0)) )
A5:
now 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;
( 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
;
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;
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;
( 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;
( 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;
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; 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
;
verum