theorem Th5: :: TAYLOR_2:5

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