thus exp_R " is_differentiable_on dom (exp_R " ) by Th16, FDIFF_2:45; :: thesis: for x being real number st x in dom (exp_R " ) holds
diff (exp_R " ),x = 1 / x
let x be real number ; :: 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:55;
diff exp_R ,((exp_R " ) . x) = exp_R . ((exp_R " ) . x) by Th16
.= x by A2, FUNCT_1:57 ;
hence diff (exp_R " ),x = 1 / x by A1, Th16, FDIFF_2:45; :: thesis: verum