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

(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