thus
exp_R " is_differentiable_on dom (exp_R ")
by Th16, FDIFF_2:45; :: thesis: for x being Real st x in dom (exp_R ") holds

diff ((exp_R "),x) = 1 / x

let x be Real; :: thesis: ( x in dom (exp_R ") implies diff ((exp_R "),x) = 1 / x )

assume A1: x in dom (exp_R ") ; :: thesis: diff ((exp_R "),x) = 1 / x

A2: x in rng exp_R by A1, FUNCT_1:33;

diff (exp_R,((exp_R ") . x)) = exp_R . ((exp_R ") . x) by Th16

.= x by A2, FUNCT_1:35 ;

hence diff ((exp_R "),x) = 1 / x by A1, Th16, FDIFF_2:45; :: thesis: verum

diff ((exp_R "),x) = 1 / x

let x be Real; :: thesis: ( x in dom (exp_R ") implies diff ((exp_R "),x) = 1 / x )

assume A1: x in dom (exp_R ") ; :: thesis: diff ((exp_R "),x) = 1 / x

A2: x in rng exp_R by A1, FUNCT_1:33;

diff (exp_R,((exp_R ") . x)) = exp_R . ((exp_R ") . x) by Th16

.= x by A2, FUNCT_1:35 ;

hence diff ((exp_R "),x) = 1 / x by A1, Th16, FDIFF_2:45; :: thesis: verum