theorem Th74: :: MESFUN15:72

for f being PartFunc of REAL,REAL
for a being Real st right_closed_halfline a c= dom f & max+ f is_+infty_ext_Riemann_integrable_on a & max- f is_+infty_ext_Riemann_integrable_on a holds
( f is_+infty_ext_Riemann_integrable_on a & improper_integral_+infty (f,a) = (improper_integral_+infty ((max+ f),a)) - (improper_integral_+infty ((max- f),a)) )