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 that
A1: Z c= dom (f1 / f2) and
A2: 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) ) )
Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, RFUNCT_1:def 1;
then A3: 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 A3;
then x in dom (f2 ^) by RFUNCT_1:def 2;
hence f2 . x <> 0 by RFUNCT_1:3; :: 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 A2;
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