theorem Th73: :: MESFUN15:71

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