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