theorem :: FDIFF_6:17

for a being Real
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (log (number_e,a))) (#) ((- (exp_R * f1)) (#) f2)) & ( for x being Real st x in Z holds
( f1 . x = - (x * (log (number_e,a))) & f2 . x = x + (1 / (log (number_e,a))) ) ) & a > 0 & a <> 1 holds
( (1 / (log (number_e,a))) (#) ((- (exp_R * f1)) (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / (log (number_e,a))) (#) ((- (exp_R * f1)) (#) f2)) `| Z) . x = x / (a #R x) ) )