theorem :: FDIFF_5:21

for Z being open Subset of REAL
for g being PartFunc of REAL,REAL st Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds
x > 0 ) holds
( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) )