let f, g be PartFunc of REAL,REAL; :: thesis: for b being Real st left_closed_halfline b c= dom f & left_closed_halfline b c= dom g & f is_-infty_improper_integrable_on b & g is_-infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_-infty (g,b) = +infty ) & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_-infty (g,b) = -infty ) holds
( f - g is_-infty_improper_integrable_on b & improper_integral_-infty ((f - g),b) = (improper_integral_-infty (f,b)) - (improper_integral_-infty (g,b)) )
let b be Real; :: thesis: ( left_closed_halfline b c= dom f & left_closed_halfline b c= dom g & f is_-infty_improper_integrable_on b & g is_-infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_-infty (g,b) = +infty ) & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_-infty (g,b) = -infty ) implies ( f - g is_-infty_improper_integrable_on b & improper_integral_-infty ((f - g),b) = (improper_integral_-infty (f,b)) - (improper_integral_-infty (g,b)) ) )
assume that
A1: left_closed_halfline b c= dom f and
A2: left_closed_halfline b c= dom g and
A3: f is_-infty_improper_integrable_on b and
A4: g is_-infty_improper_integrable_on b and
A5: ( not improper_integral_-infty (f,b) = +infty or not improper_integral_-infty (g,b) = +infty ) and
A6: ( not improper_integral_-infty (f,b) = -infty or not improper_integral_-infty (g,b) = -infty ) ; :: thesis: ( f - g is_-infty_improper_integrable_on b & improper_integral_-infty ((f - g),b) = (improper_integral_-infty (f,b)) - (improper_integral_-infty (g,b)) )
A7: dom (- g) = dom g by VALUED_1:8;
A8: - g is_-infty_improper_integrable_on b by A2, A4, Th43;

A9: now :: thesis: ( improper_integral_-infty (f,b) = +infty implies not improper_integral_-infty ((- g),b) = -infty )

assume A10: ( improper_integral_-infty (f,b) = +infty & improper_integral_-infty ((- g),b) = -infty ) ; :: thesis: contradiction
then - (improper_integral_-infty (g,b)) = - +infty by A2, A4, Th43, XXREAL_3:6;
hence contradiction by A5, A10, XXREAL_3:10; :: thesis: verum

end;

A11: now :: thesis: ( improper_integral_-infty (f,b) = -infty implies not improper_integral_-infty ((- g),b) = +infty )

assume A12: ( improper_integral_-infty (f,b) = -infty & improper_integral_-infty ((- g),b) = +infty ) ; :: thesis: contradiction
then - (improper_integral_-infty (g,b)) = - -infty by A2, A4, Th43, XXREAL_3:5;
hence contradiction by A6, A12, XXREAL_3:10; :: thesis: verum

end;

hence f - g is_-infty_improper_integrable_on b by A1, A2, A7, A3, A8, A9, Th45; :: thesis: improper_integral_-infty ((f - g),b) = (improper_integral_-infty (f,b)) - (improper_integral_-infty (g,b))
improper_integral_-infty ((f - g),b) = (improper_integral_-infty (f,b)) + (improper_integral_-infty ((- g),b)) by A1, A2, A7, A3, A8, A9, A11, Th45
.= (improper_integral_-infty (f,b)) + (- (improper_integral_-infty (g,b))) by A2, A4, Th43 ;
hence improper_integral_-infty ((f - g),b) = (improper_integral_-infty (f,b)) - (improper_integral_-infty (g,b)) by XXREAL_3:def 4; :: thesis: verum