theorem :: FDIFF_6:10

for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((f2 ^) + (ln * (f1 / f2))) & ( for x being Real st x in Z holds
( f2 . x = x & f2 . x > 0 & f1 . x = x - 1 & f1 . x > 0 ) ) holds
( (f2 ^) + (ln * (f1 / f2)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((f2 ^) + (ln * (f1 / f2))) `| Z) . x = 1 / ((x ^2) * (x - 1)) ) )