let Z be open Subset of REAL; :: thesis: ( Z c= dom () implies ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = (exp_R . ()) * () ) ) )

A1: for x being Real st x in Z holds
exp_R * exp_R is_differentiable_in x
proof end;
assume A3: Z c= dom () ; :: thesis: ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = (exp_R . ()) * () ) )

then A4: exp_R * exp_R is_differentiable_on Z by ;
for x being Real st x in Z holds
(() `| Z) . x = (exp_R . ()) * ()
proof
let x be Real; :: thesis: ( x in Z implies (() `| Z) . x = (exp_R . ()) * () )
assume A5: x in Z ; :: thesis: (() `| Z) . x = (exp_R . ()) * ()
A6: exp_R is_differentiable_in exp_R . x by SIN_COS:65;
exp_R is_differentiable_in x by SIN_COS:65;
then diff ((),x) = (diff (exp_R,())) * (diff (exp_R,x)) by
.= (exp_R . ()) * (diff (exp_R,x)) by SIN_COS:65
.= (exp_R . ()) * () by SIN_COS:65 ;
hence ((exp_R * exp_R) `| Z) . x = (exp_R . ()) * () by ; :: thesis: verum
end;
hence ( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() `| Z) . x = (exp_R . ()) * () ) ) by ; :: thesis: verum