let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st x0 in dom f2 & f1 is_continuous_in x0 & f1 . x0 <> 0 & f2 is_continuous_in x0 holds
f2 / f1 is_continuous_in x0
let f1, f2 be PartFunc of REAL,REAL; ( x0 in dom f2 & f1 is_continuous_in x0 & f1 . x0 <> 0 & f2 is_continuous_in x0 implies f2 / f1 is_continuous_in x0 )
assume A1:
x0 in dom f2
; ( not f1 is_continuous_in x0 or not f1 . x0 <> 0 or not f2 is_continuous_in x0 or f2 / f1 is_continuous_in x0 )
assume that
A2:
f1 is_continuous_in x0
and
A3:
f1 . x0 <> 0
and
A4:
f2 is_continuous_in x0
; f2 / f1 is_continuous_in x0
not f1 . x0 in {0}
by A3, TARSKI:def 1;
then A5:
not x0 in f1 " {0}
by FUNCT_1:def 7;
x0 in dom f1
by A3, FUNCT_1:def 2;
then
x0 in (dom f1) \ (f1 " {0})
by A5, XBOOLE_0:def 5;
then
x0 in dom (f1 ^)
by RFUNCT_1:def 2;
then A6:
x0 in (dom (f1 ^)) /\ (dom f2)
by A1, XBOOLE_0:def 4;
f1 ^ is_continuous_in x0
by A2, A3, Th10;
then
f2 (#) (f1 ^) is_continuous_in x0
by A4, A6, Th7;
hence
f2 / f1 is_continuous_in x0
by RFUNCT_1:31; verum