let a be Real; :: thesis: for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom () & ( for x being Real st x in Z holds
f . x = x * (log (number_e,a)) ) & a > 0 holds
( exp_R * f is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = (a #R x) * (log (number_e,a)) ) )

let Z be open Subset of REAL; :: thesis: for f being PartFunc of REAL,REAL st Z c= dom () & ( for x being Real st x in Z holds
f . x = x * (log (number_e,a)) ) & a > 0 holds
( exp_R * f is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = (a #R x) * (log (number_e,a)) ) )

let f be PartFunc of REAL,REAL; :: thesis: ( Z c= dom () & ( for x being Real st x in Z holds
f . x = x * (log (number_e,a)) ) & a > 0 implies ( exp_R * f is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = (a #R x) * (log (number_e,a)) ) ) )

assume that
A1: Z c= dom () and
A2: for x being Real st x in Z holds
f . x = x * (log (number_e,a)) and
A3: a > 0 ; :: thesis: ( exp_R * f is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = (a #R x) * (log (number_e,a)) ) )

for y being object st y in Z holds
y in dom f by ;
then A4: Z c= dom f by TARSKI:def 3;
A5: for x being Real st x in Z holds
f . x = ((log (number_e,a)) * x) + 0 by A2;
then A6: f is_differentiable_on Z by ;
A7: for x being Real st x in Z holds
exp_R * f is_differentiable_in x
proof end;
then A8: exp_R * f is_differentiable_on Z by ;
for x being Real st x in Z holds
(() `| Z) . x = (a #R x) * (log (number_e,a))
proof
let x be Real; :: thesis: ( x in Z implies (() `| Z) . x = (a #R x) * (log (number_e,a)) )
assume A9: x in Z ; :: thesis: (() `| Z) . x = (a #R x) * (log (number_e,a))
then f is_differentiable_in x by ;
then diff ((),x) = (exp_R . (f . x)) * (diff (f,x)) by TAYLOR_1:19
.= (exp_R . (f . x)) * ((f `| Z) . x) by
.= (exp_R . (f . x)) * (log (number_e,a)) by
.= (exp_R . (x * (log (number_e,a)))) * (log (number_e,a)) by A2, A9
.= (a #R x) * (log (number_e,a)) by ;
hence ((exp_R * f) `| Z) . x = (a #R x) * (log (number_e,a)) by ; :: thesis: verum
end;
hence ( exp_R * f is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = (a #R x) * (log (number_e,a)) ) ) by ; :: thesis: verum