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_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)) )
let a, b be Real; :: thesis: ( 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 ) implies ( 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)) ) )
assume that
A1: a < b and
A2: ].a,b.] c= dom f and
A3: ].a,b.] c= dom g and
A4: f is_left_improper_integrable_on a,b and
A5: g is_left_improper_integrable_on a,b and
A6: ( not left_improper_integral (f,a,b) = +infty or not left_improper_integral (g,a,b) = +infty ) and
A7: ( not left_improper_integral (f,a,b) = -infty or not left_improper_integral (g,a,b) = -infty ) ; :: thesis: ( 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)) )
A8: dom (- g) = dom g by VALUED_1:8;
A9: - g is_left_improper_integrable_on a,b by A1, A3, A5, Th55;

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

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

end;

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

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

end;

hence f - g is_left_improper_integrable_on a,b by A1, A2, A3, A8, A4, A9, A10, Th57; :: thesis: left_improper_integral ((f - g),a,b) = (left_improper_integral (f,a,b)) - (left_improper_integral (g,a,b))
left_improper_integral ((f - g),a,b) = (left_improper_integral (f,a,b)) + (left_improper_integral ((- g),a,b)) by A1, A2, A3, A8, A4, A9, A10, A12, Th57
.= (left_improper_integral (f,a,b)) + (- (left_improper_integral (g,a,b))) by A1, A3, A5, Th55 ;
hence left_improper_integral ((f - g),a,b) = (left_improper_integral (f,a,b)) - (left_improper_integral (g,a,b)) by XXREAL_3:def 4; :: thesis: verum