let x0 be positive Real; :: thesis: exp_R ^ is_differentiable_on ].0,x0.[
set F = exp_R ^ ;
set Z = ].0,x0.[;
for x being Real st x in ].0,x0.[ holds
exp_R ^ is_differentiable_in x by Lm24;
hence exp_R ^ is_differentiable_on ].0,x0.[ by Lm23A, FDIFF_1:9; :: thesis: verum