for Z being open Subset of REAL
for n being Nat holds (diff (exp_R,Z)) . n = exp_R | Z