for Z being open Subset of REAL holds (diff ((exp_R (#) cos),Z)) . 2 = 2 (#) ((exp_R (#) (- sin)) | Z)