theorem :: FDIFF_6:37

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