let x0 be real number ; :: thesis: for f2, f1 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 f2, f1 be PartFunc of REAL ,REAL ; :: thesis: ( 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 Z1: x0 in dom f2 ; :: thesis: ( 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 Z: ( f1 is_continuous_in x0 & f1 . x0 <> 0 & f2 is_continuous_in x0 ) ; :: thesis: f2 / f1 is_continuous_in x0
then Y: x0 in dom f1 by FUNCT_1:def 4;
not f1 . x0 in {0 } by Z, TARSKI:def 1;
then not x0 in f1 " {0 } by FUNCT_1:def 13;
then x0 in (dom f1) \ (f1 " {0 }) by Y, XBOOLE_0:def 5;
then x0 in dom (f1 ^ ) by RFUNCT_1:def 8;
then X: x0 in (dom (f1 ^ )) /\ (dom f2) by Z1, XBOOLE_0:def 4;
( f1 ^ is_continuous_in x0 & f2 is_continuous_in x0 ) by Th10, Z;
then f2 (#) (f1 ^ ) is_continuous_in x0 by Th7, X;
hence f2 / f1 is_continuous_in x0 by RFUNCT_1:47; :: thesis: verum