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 2
.= dom f1 ;
(f1 ^) | X is continuous by A2, A3, Th22;
then (f2 (#) (f1 ^)) | X is continuous by A1, A4, A5, Th18;
hence (f2 / f1) | X is continuous by RFUNCT_1:31; :: thesis: verum