A1: exp_R ^ is Function of REAL,REAL by Lm23A, FUNCT_2:def 1;
for x being set st x in REAL holds
exp_R . x <> 0 by SIN_COS:54;
then exp_R ^ is_differentiable_on REAL by SIN_COS:66, INTEGRA7:9;
then for x being Real holds exp_R ^ is_differentiable_in x by XREAL_0:def 1;
hence ( exp_R ^ is_differentiable_on REAL & exp_R ^ is differentiable Function of REAL,REAL & exp_R is differentiable ) by Lm23A, A1, POLYDIFF:def 2, SIN_COS:65; :: thesis: verum