theorem Th32: :: INTEGRA8:32

exp_R `| REAL = exp_R