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 A1: 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 that
A2: f1 | X is continuous and
A3: f1 " {0 } = {} and
A4: f2 | X is continuous ; :: thesis: (f2 / f1) | X is continuous
A5: dom (f1 ^ ) = (dom f1) \ {} by A3, RFUNCT_1:def 8
.= dom f1 ;
(f1 ^ ) | X is continuous by A2, A3, Th23;
then (f2 (#) (f1 ^ )) | X is continuous by A1, A4, A5, Th19;
hence (f2 / f1) | X is continuous by RFUNCT_1:47; :: thesis: verum