let a, b be Real; :: thesis: for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL ,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x + a & f2 . x = x - b ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2 ) ) )
let Z be open Subset of REAL ; :: thesis: for f1, f2 being PartFunc of REAL ,REAL st Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x + a & f2 . x = x - b ) ) holds
( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2 ) ) )
let f1, f2 be PartFunc of REAL ,REAL ; :: thesis: ( Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x + a & f2 . x = x - b ) ) implies ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2 ) ) ) )
assume A1: ( Z c= dom (f1 / f2) & ( for x being Real st x in Z holds
( f1 . x = x + a & f2 . x = x - b ) ) ) ; :: thesis: ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2 ) ) )
then Z c= (dom f1) /\ ((dom f2) \ (f2 " {0 })) by RFUNCT_1:def 4;
then A2: ( Z c= dom f1 & Z c= (dom f2) \ (f2 " {0 }) ) by XBOOLE_1:18;
for x being Real st x in Z holds
f2 . x <> 0

proof

let x be Real; :: thesis: ( x in Z implies f2 . x <> 0 )
assume x in Z ; :: thesis: f2 . x <> 0
then x in (dom f2) \ (f2 " {0 }) by A2;
then x in dom (f2 ^ ) by RFUNCT_1:def 8;
hence f2 . x <> 0 by RFUNCT_1:13; :: thesis: verum

end;

then for x being Real st x in Z holds
( f1 . x = x - (- a) & f2 . x = x - b & f2 . x <> 0 ) by A1;
hence ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds
((f1 / f2) `| Z) . x = ((- a) - b) / ((x - b) ^2 ) ) ) by A1, FDIFF_5:3; :: thesis: verum