let X be set ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f1 " {0 } = {} & f2 | X is continuous holds
(f2 / f1) | X is continuous
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( X c= (dom f1) /\ (dom f2) & f1 | X is continuous & f1 " {0 } = {} & f2 | X is continuous implies (f2 / f1) | X is continuous )
assume Z: X c= (dom f1) /\ (dom f2) ; :: thesis: ( not f1 | X is continuous or not f1 " {0 } = {} or not f2 | X is continuous or (f2 / f1) | X is continuous )
assume Z1: ( f1 | X is continuous & f1 " {0 } = {} & f2 | X is continuous ) ; :: thesis: (f2 / f1) | X is continuous
then T: dom (f1 ^ ) = (dom f1) \ {} by RFUNCT_1:def 8
.= dom f1 ;
( (f1 ^ ) | X is continuous & f2 | X is continuous ) by Th23, Z1;
then (f2 (#) (f1 ^ )) | X is continuous by Th19, Z, T;
hence (f2 / f1) | X is continuous by RFUNCT_1:47; :: thesis: verum