theorem Th72: :: MESFUN15:70
for f being PartFunc of REAL,REAL
for a, b being Real st [.a,b.[ c= dom f & max+ f is_right_ext_Riemann_integrable_on a,b & max- f is_right_ext_Riemann_integrable_on a,b holds
( f is_right_ext_Riemann_integrable_on a,b & right_improper_integral (f,a,b) = (right_improper_integral ((max+ f),a,b)) - (right_improper_integral ((max- f),a,b)) )