for Z being open Subset of REAL holds
( exp_R `| Z = exp_R | Z & dom (exp_R | Z) = Z )