for Z being open Subset of REAL
for n being Element of NAT holds exp_R is_differentiable_on n,Z