let f, g be PartFunc of REAL,REAL; :: thesis: for x0 being Real st x0 in (dom f) /\ (dom g) & ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f & [.x0,(x0 + r).] c= dom g & f is_differentiable_on ].x0,(x0 + r).[ & g is_differentiable_on ].x0,(x0 + r).[ & ].x0,(x0 + r).[ c= dom (f / g) & [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) holds
( f / g is_right_convergent_in x0 & ex r being Real st
( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) )
let x0 be Real; :: thesis: ( x0 in (dom f) /\ (dom g) & ex r being Real st
( r > 0 & [.x0,(x0 + r).] c= dom f & [.x0,(x0 + r).] c= dom g & f is_differentiable_on ].x0,(x0 + r).[ & g is_differentiable_on ].x0,(x0 + r).[ & ].x0,(x0 + r).[ c= dom (f / g) & [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) & f . x0 = 0 & g . x0 = 0 & f is_continuous_in x0 & g is_continuous_in x0 & (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) implies ( f / g is_right_convergent_in x0 & ex r being Real st
( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) ) )
assume A1: x0 in (dom f) /\ (dom g) ; :: thesis: ( for r being Real holds
( not r > 0 or not [.x0,(x0 + r).] c= dom f or not [.x0,(x0 + r).] c= dom g or not f is_differentiable_on ].x0,(x0 + r).[ or not g is_differentiable_on ].x0,(x0 + r).[ or not ].x0,(x0 + r).[ c= dom (f / g) or not [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) or not f . x0 = 0 or not g . x0 = 0 or not f is_continuous_in x0 or not g is_continuous_in x0 or not (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ) or ( f / g is_right_convergent_in x0 & ex r being Real st
( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) ) )
given r being Real such that A2: r > 0 and
A3: [.x0,(x0 + r).] c= dom f and
A4: [.x0,(x0 + r).] c= dom g and
A5: f is_differentiable_on ].x0,(x0 + r).[ and
A6: g is_differentiable_on ].x0,(x0 + r).[ and
A7: ].x0,(x0 + r).[ c= dom (f / g) and
A8: [.x0,(x0 + r).] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) and
A9: ( f . x0 = 0 & g . x0 = 0 ) and
A10: f is_continuous_in x0 and
A11: g is_continuous_in x0 and
A12: (f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[) is_right_convergent_in x0 ; :: thesis: ( f / g is_right_convergent_in x0 & ex r being Real st
( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) )
A13: ].x0,(x0 + r).[ c= [.x0,(x0 + r).] by XXREAL_1:25;
then A14: ].x0,(x0 + r).[ c= dom g by A4;
A15: ].x0,(x0 + r).[ c= dom f by A3, A13;
A16: for x being Real st x0 < x & x < x0 + r holds
ex c being Real st
( c in ].x0,x.[ & (f / g) . x = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . c )

proof

let x be Real; :: thesis: ( x0 < x & x < x0 + r implies ex c being Real st
( c in ].x0,x.[ & (f / g) . x = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . c ) )
assume that
A17: x0 < x and
A18: x < x0 + r ; :: thesis: ex c being Real st
( c in ].x0,x.[ & (f / g) . x = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . c )
set f1 = ((f . x) (#) g) - ((g . x) (#) f);
A19: dom ((g . x) (#) f) = dom f by VALUED_1:def 5;
A20: dom ((f . x) (#) g) = dom g by VALUED_1:def 5;
then A21: dom (((f . x) (#) g) - ((g . x) (#) f)) = (dom f) /\ (dom g) by A19, VALUED_1:12;
A22: [.x0,x.] c= [.x0,(x0 + r).]

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in [.x0,x.] or y in [.x0,(x0 + r).] )
assume A23: y in [.x0,x.] ; :: thesis: y in [.x0,(x0 + r).]
then reconsider y = y as Real ;
y <= x by A23, XXREAL_1:1;
then A24: y <= x0 + r by A18, XXREAL_0:2;
x0 <= y by A23, XXREAL_1:1;
hence y in [.x0,(x0 + r).] by A24, XXREAL_1:1; :: thesis: verum

end;

then A25: ( [.x0,x.] c= dom f & [.x0,x.] c= dom g ) by A3, A4;
then A26: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A21, XBOOLE_1:19;
A27: x in [.x0,x.] by A17, XXREAL_1:1;
then x in dom (((f . x) (#) g) - ((g . x) (#) f)) by A26;
then A28: x in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12;
then A29: x in dom ((f . x) (#) g) by XBOOLE_0:def 4;
A30: x in dom ((g . x) (#) f) by A28, XBOOLE_0:def 4;
A31: (((f . x) (#) g) - ((g . x) (#) f)) . x = (((f . x) (#) g) . x) - (((g . x) (#) f) . x) by A26, A27, VALUED_1:13
.= ((f . x) * (g . x)) - (((g . x) (#) f) . x) by A29, VALUED_1:def 5
.= ((g . x) * (f . x)) - ((g . x) * (f . x)) by A30, VALUED_1:def 5
.= 0 ;
A32: ].x0,(x0 + r).[ c= dom f by A3, A13;
not x in {x0} by A17, TARSKI:def 1;
then A33: x in [.x0,x.] \ {x0} by A27, XBOOLE_0:def 5;
x in { g1 where g1 is Real : ( x0 < g1 & g1 < x0 + r ) } by A17, A18;
then A34: x in ].x0,(x0 + r).[ by RCOMP_1:def 2;
A35: x0 in [.x0,x.] by A17, XXREAL_1:1;
then x0 in dom (((f . x) (#) g) - ((g . x) (#) f)) by A26;
then A36: x0 in (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by VALUED_1:12;
then A37: x0 in dom ((f . x) (#) g) by XBOOLE_0:def 4;
A38: [.x0,x.] c= dom (((f . x) (#) g) - ((g . x) (#) f)) by A25, A21, XBOOLE_1:19;
A39: x0 in dom ((g . x) (#) f) by A36, XBOOLE_0:def 4;
A40: ].x0,(x0 + r).[ c= dom g by A4, A13;
A41: ].x0,x.[ c= ].x0,(x0 + r).[

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in ].x0,x.[ or y in ].x0,(x0 + r).[ )
assume y in ].x0,x.[ ; :: thesis: y in ].x0,(x0 + r).[
then y in { g2 where g2 is Real : ( x0 < g2 & g2 < x ) } by RCOMP_1:def 2;
then consider g2 being Real such that
A42: ( g2 = y & x0 < g2 ) and
A43: g2 < x ;
g2 < x0 + r by A18, A43, XXREAL_0:2;
then y in { g3 where g3 is Real : ( x0 < g3 & g3 < x0 + r ) } by A42;
hence y in ].x0,(x0 + r).[ by RCOMP_1:def 2; :: thesis: verum

end;

then A44: ].x0,x.[ c= dom ((f . x) (#) g) by A14, A20;
x0 in dom f by A1, XBOOLE_0:def 4;
then A45: {x0,x} c= dom f by A34, A32, ZFMISC_1:32;
].x0,x.[ c= dom f by A41, A32;
then ].x0,x.[ \/ {x0,x} c= dom f by A45, XBOOLE_1:8;
then A46: [.x0,x.] c= dom f by A17, XXREAL_1:128;
x0 in dom g by A1, XBOOLE_0:def 4;
then A47: {x0,x} c= dom g by A34, A40, ZFMISC_1:32;
].x0,x.[ c= dom g by A41, A40;
then ].x0,x.[ \/ {x0,x} c= dom g by A47, XBOOLE_1:8;
then A48: [.x0,x.] c= dom g by A17, XXREAL_1:128;
g is_differentiable_in x by A6, A34, FDIFF_1:9;
then A49: g is_continuous_in x by FDIFF_1:24;
for s being Real_Sequence st rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.] holds
( g /* s is convergent & g . (lim s) = lim (g /* s) )

proof

let s be Real_Sequence; :: thesis: ( rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.] implies ( g /* s is convergent & g . (lim s) = lim (g /* s) ) )
assume that
A50: rng s c= [.x0,x.] and
A51: s is convergent and
A52: lim s in [.x0,x.] ; :: thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) )
set z = lim s;
A53: rng s c= dom g by A48, A50;
A54: lim s in ].x0,x.[ \/ {x0,x} by A17, A52, XXREAL_1:128;

now :: thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) )

per cases ( lim s in ].x0,x.[ or lim s in {x0,x} ) by A54, XBOOLE_0:def 3;

suppose lim s in ].x0,x.[ ; :: thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) )

then g is_differentiable_in lim s by A6, A41, FDIFF_1:9;
then g is_continuous_in lim s by FDIFF_1:24;
hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A51, A53, FCONT_1:def 1; :: thesis: verum

end;

suppose A55: lim s in {x0,x} ; :: thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) )

now :: thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) )

per cases ( lim s = x0 or lim s = x ) by A55, TARSKI:def 2;

suppose lim s = x0 ; :: thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) )

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A11, A51, A53, FCONT_1:def 1; :: thesis: verum

end;

suppose lim s = x ; :: thesis: ( g /* s is convergent & g . (lim s) = lim (g /* s) )

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) by A49, A51, A53, FCONT_1:def 1; :: thesis: verum

end;

end;

end;

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ; :: thesis: verum

end;

end;

end;

hence ( g /* s is convergent & g . (lim s) = lim (g /* s) ) ; :: thesis: verum

end;

then g | [.x0,x.] is continuous by A48, FCONT_1:13;
then A56: ((f . x) (#) g) | [.x0,x.] is continuous by A4, A22, FCONT_1:20, XBOOLE_1:1;
f is_differentiable_in x by A5, A34, FDIFF_1:9;
then A57: f is_continuous_in x by FDIFF_1:24;
for s being Real_Sequence st rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.] holds
( f /* s is convergent & f . (lim s) = lim (f /* s) )

proof

let s be Real_Sequence; :: thesis: ( rng s c= [.x0,x.] & s is convergent & lim s in [.x0,x.] implies ( f /* s is convergent & f . (lim s) = lim (f /* s) ) )
assume that
A58: rng s c= [.x0,x.] and
A59: s is convergent and
A60: lim s in [.x0,x.] ; :: thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) )
set z = lim s;
A61: rng s c= dom f by A46, A58;
A62: lim s in ].x0,x.[ \/ {x0,x} by A17, A60, XXREAL_1:128;

now :: thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) )

per cases ( lim s in ].x0,x.[ or lim s in {x0,x} ) by A62, XBOOLE_0:def 3;

suppose lim s in ].x0,x.[ ; :: thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) )

then f is_differentiable_in lim s by A5, A41, FDIFF_1:9;
then f is_continuous_in lim s by FDIFF_1:24;
hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A59, A61, FCONT_1:def 1; :: thesis: verum

end;

suppose A63: lim s in {x0,x} ; :: thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) )

now :: thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) )

per cases ( lim s = x0 or lim s = x ) by A63, TARSKI:def 2;

suppose lim s = x0 ; :: thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) )

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A10, A59, A61, FCONT_1:def 1; :: thesis: verum

end;

suppose lim s = x ; :: thesis: ( f /* s is convergent & f . (lim s) = lim (f /* s) )

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) by A57, A59, A61, FCONT_1:def 1; :: thesis: verum

end;

end;

end;

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ; :: thesis: verum

end;

end;

end;

hence ( f /* s is convergent & f . (lim s) = lim (f /* s) ) ; :: thesis: verum

end;

then f | [.x0,x.] is continuous by A46, FCONT_1:13;
then ((g . x) (#) f) | [.x0,x.] is continuous by A3, A22, FCONT_1:20, XBOOLE_1:1;
then A64: (((f . x) (#) g) - ((g . x) (#) f)) | [.x0,x.] is continuous by A20, A19, A21, A38, A56, FCONT_1:18;
g is_differentiable_on ].x0,x.[ by A6, A41, FDIFF_1:26;
then A65: (f . x) (#) g is_differentiable_on ].x0,x.[ by A44, FDIFF_1:20;
A66: ].x0,x.[ c= dom ((g . x) (#) f) by A15, A41, A19;
then ].x0,x.[ c= (dom ((f . x) (#) g)) /\ (dom ((g . x) (#) f)) by A44, XBOOLE_1:19;
then A67: ].x0,x.[ c= dom (((f . x) (#) g) - ((g . x) (#) f)) by VALUED_1:12;
f is_differentiable_on ].x0,x.[ by A5, A41, FDIFF_1:26;
then A68: (g . x) (#) f is_differentiable_on ].x0,x.[ by A66, FDIFF_1:20;
(((f . x) (#) g) - ((g . x) (#) f)) . x0 = (((f . x) (#) g) . x0) - (((g . x) (#) f) . x0) by A26, A35, VALUED_1:13
.= ((f . x) * (g . x0)) - (((g . x) (#) f) . x0) by A37, VALUED_1:def 5
.= 0 - ((g . x) * 0) by A9, A39, VALUED_1:def 5
.= 0 ;
then consider t being Real such that
A69: t in ].x0,x.[ and
A70: diff ((((f . x) (#) g) - ((g . x) (#) f)),t) = 0 by A17, A64, A68, A67, A65, A26, A31, FDIFF_1:19, ROLLE:1;
A71: (g . x) (#) f is_differentiable_in t by A68, A69, FDIFF_1:9;
A72: f is_differentiable_in t by A5, A41, A69, FDIFF_1:9;
(f . x) (#) g is_differentiable_in t by A65, A69, FDIFF_1:9;
then 0 = (diff (((f . x) (#) g),t)) - (diff (((g . x) (#) f),t)) by A70, A71, FDIFF_1:14;
then A73: 0 = (diff (((f . x) (#) g),t)) - ((g . x) * (diff (f,t))) by A72, FDIFF_1:15;
A74: (dom (f `| ].x0,(x0 + r).[)) /\ ((dom (g `| ].x0,(x0 + r).[)) \ ((g `| ].x0,(x0 + r).[) " {0})) c= (dom (g `| ].x0,(x0 + r).[)) \ ((g `| ].x0,(x0 + r).[) " {0}) by XBOOLE_1:17;
A75: (dom f) /\ ((dom g) \ (g " {0})) c= (dom g) \ (g " {0}) by XBOOLE_1:17;

now :: thesis: for y being object st y in [.x0,x.] \ {x0} holds
y in ].x0,(x0 + r).[

let y be object ; :: thesis: ( y in [.x0,x.] \ {x0} implies y in ].x0,(x0 + r).[ )
assume A76: y in [.x0,x.] \ {x0} ; :: thesis: y in ].x0,(x0 + r).[
then y in [.x0,x.] by XBOOLE_0:def 5;
then y in { g4 where g4 is Real : ( x0 <= g4 & g4 <= x ) } by RCOMP_1:def 1;
then consider g4 being Real such that
A77: g4 = y and
A78: x0 <= g4 and
A79: g4 <= x ;
not y in {x0} by A76, XBOOLE_0:def 5;
then x0 <> g4 by A77, TARSKI:def 1;
then A80: x0 < g4 by A78, XXREAL_0:1;
g4 < x0 + r by A18, A79, XXREAL_0:2;
then y in { g5 where g5 is Real : ( x0 < g5 & g5 < x0 + r ) } by A77, A80;
hence y in ].x0,(x0 + r).[ by RCOMP_1:def 2; :: thesis: verum

end;

then [.x0,x.] \ {x0} c= ].x0,(x0 + r).[ ;
then A81: [.x0,x.] \ {x0} c= dom (f / g) by A7;
then [.x0,x.] \ {x0} c= (dom f) /\ ((dom g) \ (g " {0})) by RFUNCT_1:def 1;
then [.x0,x.] \ {x0} c= (dom g) \ (g " {0}) by A75;
then A82: ( x in dom g & not x in g " {0} ) by A33, XBOOLE_0:def 5;

A83: now :: thesis: not g . x = 0

assume g . x = 0 ; :: thesis: contradiction
then g . x in {0} by TARSKI:def 1;
hence contradiction by A82, FUNCT_1:def 7; :: thesis: verum

end;

take t ; :: thesis: ( t in ].x0,x.[ & (f / g) . x = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . t )
].x0,x.[ c= [.x0,x.] by XXREAL_1:25;
then A84: t in [.x0,x.] by A69;
x0 <= x0 + r by A2, XREAL_1:29;
then x0 in { g6 where g6 is Real : ( x0 <= g6 & g6 <= x0 + r ) } ;
then ( ].x0,(x0 + r).[ c= [.x0,(x0 + r).] & x0 in [.x0,(x0 + r).] ) by RCOMP_1:def 1, XXREAL_1:25;
then [.x0,x.] c= [.x0,(x0 + r).] by A34, XXREAL_2:def 12;
then A85: [.x0,x.] c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) by A8;
then [.x0,x.] c= (dom (f `| ].x0,(x0 + r).[)) /\ ((dom (g `| ].x0,(x0 + r).[)) \ ((g `| ].x0,(x0 + r).[) " {0})) by RFUNCT_1:def 1;
then [.x0,x.] c= (dom (g `| ].x0,(x0 + r).[)) \ ((g `| ].x0,(x0 + r).[) " {0}) by A74;
then A86: ( t in dom (g `| ].x0,(x0 + r).[) & not t in (g `| ].x0,(x0 + r).[) " {0} ) by A84, XBOOLE_0:def 5;

A87: now :: thesis: not diff (g,t) = 0

assume diff (g,t) = 0 ; :: thesis: contradiction
then (g `| ].x0,(x0 + r).[) . t = 0 by A6, A41, A69, FDIFF_1:def 7;
then (g `| ].x0,(x0 + r).[) . t in {0} by TARSKI:def 1;
hence contradiction by A86, FUNCT_1:def 7; :: thesis: verum

end;

g is_differentiable_in t by A6, A41, A69, FDIFF_1:9;
then 0 = ((f . x) * (diff (g,t))) - ((g . x) * (diff (f,t))) by A73, FDIFF_1:15;
then (f . x) / (g . x) = (diff (f,t)) / (diff (g,t)) by A83, A87, XCMPLX_1:94;
then (f . x) * ((g . x) ") = (diff (f,t)) / (diff (g,t)) by XCMPLX_0:def 9;
then (f . x) * ((g . x) ") = (diff (f,t)) * ((diff (g,t)) ") by XCMPLX_0:def 9;
then (f / g) . x = (diff (f,t)) * ((diff (g,t)) ") by A81, A33, RFUNCT_1:def 1;
then (f / g) . x = ((f `| ].x0,(x0 + r).[) . t) * ((diff (g,t)) ") by A5, A41, A69, FDIFF_1:def 7;
then (f / g) . x = ((f `| ].x0,(x0 + r).[) . t) * (((g `| ].x0,(x0 + r).[) . t) ") by A6, A41, A69, FDIFF_1:def 7;
hence ( t in ].x0,x.[ & (f / g) . x = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . t ) by A69, A85, A84, RFUNCT_1:def 1; :: thesis: verum

end;

A88: for a being Real_Sequence st a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (right_open_halfline x0) holds
( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) )

proof

reconsider xx0 = x0 as Element of REAL by XREAL_0:def 1;
set d = seq_const x0;
let a be Real_Sequence; :: thesis: ( a is convergent & lim a = x0 & rng a c= (dom (f / g)) /\ (right_open_halfline x0) implies ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) )
assume that
A89: a is convergent and
A90: lim a = x0 and
A91: rng a c= (dom (f / g)) /\ (right_open_halfline x0) ; :: thesis: ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) )
consider k being Element of NAT such that
A92: for n being Element of NAT st k <= n holds
( x0 - r < a . n & a . n < x0 + r ) by A2, A89, A90, LIMFUNC3:7;
set a1 = a ^\ k;
defpred S₁[ Element of NAT , Real] means ( $2 in ].x0,((a ^\ k) . $1).[ & (((f / g) /* a) ^\ k) . $1 = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . $2 );

A93: now :: thesis: for n being Element of NAT holds
( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r )

let n be Element of NAT ; :: thesis: ( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r )
a . (n + k) in rng a by VALUED_0:28;
then a . (n + k) in right_open_halfline x0 by A91, XBOOLE_0:def 4;
then a . (n + k) in { g1 where g1 is Real : x0 < g1 } by XXREAL_1:230;
then ex g1 being Real st
( a . (n + k) = g1 & x0 < g1 ) ;
hence x0 < (a ^\ k) . n by NAT_1:def 3; :: thesis: (a ^\ k) . n < x0 + r
( (a ^\ k) . n = a . (n + k) & k <= n + k ) by NAT_1:12, NAT_1:def 3;
hence (a ^\ k) . n < x0 + r by A92; :: thesis: verum

end;

A94: for n being Element of NAT ex c being Element of REAL st S₁[n,c]

proof

let n be Element of NAT ; :: thesis: ex c being Element of REAL st S₁[n,c]
A95: rng (a ^\ k) c= rng a by VALUED_0:21;
( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A93;
then consider c being Real such that
A96: c in ].x0,((a ^\ k) . n).[ and
A97: (f / g) . ((a ^\ k) . n) = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . c by A16;
take c ; :: thesis: ( c is set & c is Element of REAL & S₁[n,c] )
A98: (dom (f / g)) /\ (right_open_halfline x0) c= dom (f / g) by XBOOLE_1:17;
then rng a c= dom (f / g) by A91;
then ((f / g) /* (a ^\ k)) . n = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . c by A97, A95, FUNCT_2:108, XBOOLE_1:1;
hence ( c is set & c is Element of REAL & S₁[n,c] ) by A91, A96, A98, VALUED_0:27, XBOOLE_1:1; :: thesis: verum

end;

consider b being Real_Sequence such that
A99: for n being Element of NAT holds S₁[n,b . n] from FUNCT_2:sch 3(A94);
A100: rng b c= (dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng b or x in (dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0) )
assume x in rng b ; :: thesis: x in (dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0)
then consider n being Element of NAT such that
A101: x = b . n by FUNCT_2:113;
x0 <= x0 + r by A2, XREAL_1:29;
then x0 in { g3 where g3 is Real : ( x0 <= g3 & g3 <= x0 + r ) } ;
then A102: x0 in [.x0,(x0 + r).] by RCOMP_1:def 1;
( x0 < (a ^\ k) . n & (a ^\ k) . n < x0 + r ) by A93;
then (a ^\ k) . n in { g4 where g4 is Real : ( x0 <= g4 & g4 <= x0 + r ) } ;
then (a ^\ k) . n in [.x0,(x0 + r).] by RCOMP_1:def 1;
then ( ].x0,((a ^\ k) . n).[ c= [.x0,((a ^\ k) . n).] & [.x0,((a ^\ k) . n).] c= [.x0,(x0 + r).] ) by A102, XXREAL_1:25, XXREAL_2:def 12;
then ].x0,((a ^\ k) . n).[ c= [.x0,(x0 + r).] ;
then A103: ].x0,((a ^\ k) . n).[ c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) by A8;
A104: x in ].x0,((a ^\ k) . n).[ by A99, A101;
then x in { g1 where g1 is Real : ( x0 < g1 & g1 < (a ^\ k) . n ) } by RCOMP_1:def 2;
then ex g1 being Real st
( g1 = x & x0 < g1 & g1 < (a ^\ k) . n ) ;
then x in { g2 where g2 is Real : x0 < g2 } ;
then x in right_open_halfline x0 by XXREAL_1:230;
hence x in (dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0) by A104, A103, XBOOLE_0:def 4; :: thesis: verum

end;

A105: now :: thesis: for n being Nat holds
( (seq_const x0) . n <= b . n & b . n <= (a ^\ k) . n )

let n be Nat; :: thesis: ( (seq_const x0) . n <= b . n & b . n <= (a ^\ k) . n )
A106: n in NAT by ORDINAL1:def 12;
b . n in ].x0,((a ^\ k) . n).[ by A99, A106;
then b . n in { g1 where g1 is Real : ( x0 < g1 & g1 < (a ^\ k) . n ) } by RCOMP_1:def 2;
then ex g1 being Real st
( g1 = b . n & x0 < g1 & g1 < (a ^\ k) . n ) ;
hence ( (seq_const x0) . n <= b . n & b . n <= (a ^\ k) . n ) by SEQ_1:57; :: thesis: verum

end;

A107: lim (seq_const x0) = (seq_const x0) . 0 by SEQ_4:26
.= x0 by SEQ_1:57 ;
lim (a ^\ k) = x0 by A89, A90, SEQ_4:20;
then A108: ( b is convergent & lim b = x0 ) by A89, A107, A105, SEQ_2:19, SEQ_2:20;
A109: (dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[))) /\ (right_open_halfline x0) c= dom ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) by XBOOLE_1:17;

A110: now :: thesis: ex m being Nat st
for n being Nat st m <= n holds
(((f / g) /* a) ^\ k) . n = (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) . n

reconsider m = 0 as Nat ;
take m = m; :: thesis: for n being Nat st m <= n holds
(((f / g) /* a) ^\ k) . n = (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) . n
let n be Nat; :: thesis: ( m <= n implies (((f / g) /* a) ^\ k) . n = (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) . n )
assume m <= n ; :: thesis: (((f / g) /* a) ^\ k) . n = (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) . n
A111: n in NAT by ORDINAL1:def 12;
(((f / g) /* a) ^\ k) . n = ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) . (b . n) by A99, A111;
hence (((f / g) /* a) ^\ k) . n = (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) . n by A100, A109, FUNCT_2:108, XBOOLE_1:1, A111; :: thesis: verum

end;

lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ;
then A112: ((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b is convergent by A12, A108, A100, LIMFUNC2:def 8;
then A113: ((f / g) /* a) ^\ k is convergent by A110, SEQ_4:18;
lim (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)) /* b) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) by A12, A108, A100, LIMFUNC2:def 8;
then lim (((f / g) /* a) ^\ k) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) by A112, A110, SEQ_4:19;
hence ( (f / g) /* a is convergent & lim ((f / g) /* a) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) ) by A113, SEQ_4:21, SEQ_4:22; :: thesis: verum

end;

A114: for r1 being Real st x0 < r1 holds
ex t being Real st
( t < r1 & x0 < t & t in dom (f / g) ) by A2, A7, LIMFUNC2:4;
hence f / g is_right_convergent_in x0 by A88, Th2; :: thesis: ex r being Real st
( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) )
take r ; :: thesis: ( r > 0 & lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) )
thus r > 0 by A2; :: thesis: lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0)
thus lim_right ((f / g),x0) = lim_right (((f `| ].x0,(x0 + r).[) / (g `| ].x0,(x0 + r).[)),x0) by A114, A88, Th2; :: thesis: verum