for f, g being PartFunc of REAL,REAL st dom f = REAL & dom g = REAL & f is_improper_integrable_on_REAL & g is_improper_integrable_on_REAL & ( not improper_integral_on_REAL f = +infty or not improper_integral_on_REAL g = +infty ) & ( not improper_integral_on_REAL f = -infty or not improper_integral_on_REAL g = -infty ) holds
( f - g is_improper_integrable_on_REAL & improper_integral_on_REAL (f - g) = (improper_integral_on_REAL f) - (improper_integral_on_REAL g) )