for f, g being PartFunc of REAL,REAL
for a, b being Real st a < b & ].a,b.] c= dom f & ].a,b.] c= dom g & f is_left_improper_integrable_on a,b & g is_left_improper_integrable_on a,b & ( not left_improper_integral (f,a,b) = +infty or not left_improper_integral (g,a,b) = +infty ) & ( not left_improper_integral (f,a,b) = -infty or not left_improper_integral (g,a,b) = -infty ) holds
( f - g is_left_improper_integrable_on a,b & left_improper_integral ((f - g),a,b) = (left_improper_integral (f,a,b)) - (left_improper_integral (g,a,b)) )