theorem :: FDIFF_6:36

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