theorem Th27: :: INTEGRA7:27

exp_R is_integral_of exp_R , REAL