theorem :: FDIFF_6:12

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) ) )