let f, g be PartFunc of REAL,REAL; :: thesis: for a, b being Real st a < b & [.a,b.[ c= dom f & [.a,b.[ c= dom g & f is_right_improper_integrable_on a,b & g is_right_improper_integrable_on a,b & ( not right_improper_integral (f,a,b) = +infty or not right_improper_integral (g,a,b) = +infty ) & ( not right_improper_integral (f,a,b) = -infty or not right_improper_integral (g,a,b) = -infty ) holds
( f - g is_right_improper_integrable_on a,b & right_improper_integral ((f - g),a,b) = (right_improper_integral (f,a,b)) - (right_improper_integral (g,a,b)) )
let a, b be Real; :: thesis: ( a < b & [.a,b.[ c= dom f & [.a,b.[ c= dom g & f is_right_improper_integrable_on a,b & g is_right_improper_integrable_on a,b & ( not right_improper_integral (f,a,b) = +infty or not right_improper_integral (g,a,b) = +infty ) & ( not right_improper_integral (f,a,b) = -infty or not right_improper_integral (g,a,b) = -infty ) implies ( f - g is_right_improper_integrable_on a,b & right_improper_integral ((f - g),a,b) = (right_improper_integral (f,a,b)) - (right_improper_integral (g,a,b)) ) )
assume that
A1: a < b and
A2: [.a,b.[ c= dom f and
A3: [.a,b.[ c= dom g and
A4: f is_right_improper_integrable_on a,b and
A5: g is_right_improper_integrable_on a,b and
A6: ( not right_improper_integral (f,a,b) = +infty or not right_improper_integral (g,a,b) = +infty ) and
A7: ( not right_improper_integral (f,a,b) = -infty or not right_improper_integral (g,a,b) = -infty ) ; :: thesis: ( f - g is_right_improper_integrable_on a,b & right_improper_integral ((f - g),a,b) = (right_improper_integral (f,a,b)) - (right_improper_integral (g,a,b)) )
A8: dom (- g) = dom g by VALUED_1:8;
A9: - g is_right_improper_integrable_on a,b by A1, A3, A5, Th56;

A10: now :: thesis: ( right_improper_integral (f,a,b) = +infty implies not right_improper_integral ((- g),a,b) = -infty )

assume A11: ( right_improper_integral (f,a,b) = +infty & right_improper_integral ((- g),a,b) = -infty ) ; :: thesis: contradiction
then - (right_improper_integral (g,a,b)) = - +infty by A1, A3, A5, Th56, XXREAL_3:6;
hence contradiction by A6, A11, XXREAL_3:10; :: thesis: verum

end;

A12: now :: thesis: ( right_improper_integral (f,a,b) = -infty implies not right_improper_integral ((- g),a,b) = +infty )

assume A13: ( right_improper_integral (f,a,b) = -infty & right_improper_integral ((- g),a,b) = +infty ) ; :: thesis: contradiction
then - (right_improper_integral (g,a,b)) = - -infty by A1, A3, A5, Th56, XXREAL_3:5;
hence contradiction by A7, A13, XXREAL_3:10; :: thesis: verum

end;

hence f - g is_right_improper_integrable_on a,b by A1, A2, A3, A8, A4, A9, A10, Th58; :: thesis: right_improper_integral ((f - g),a,b) = (right_improper_integral (f,a,b)) - (right_improper_integral (g,a,b))
right_improper_integral ((f - g),a,b) = (right_improper_integral (f,a,b)) + (right_improper_integral ((- g),a,b)) by A1, A2, A3, A8, A4, A9, A10, A12, Th58
.= (right_improper_integral (f,a,b)) + (- (right_improper_integral (g,a,b))) by A1, A3, A5, Th56 ;
hence right_improper_integral ((f - g),a,b) = (right_improper_integral (f,a,b)) - (right_improper_integral (g,a,b)) by XXREAL_3:def 4; :: thesis: verum