let f, g be PartFunc of REAL,REAL; for a being Real st right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_improper_integrable_on a & g is_+infty_improper_integrable_on a & ( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = +infty ) & ( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = -infty ) holds
( f - g is_+infty_improper_integrable_on a & improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a)) )
let a be Real; ( right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_improper_integrable_on a & g is_+infty_improper_integrable_on a & ( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = +infty ) & ( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = -infty ) implies ( f - g is_+infty_improper_integrable_on a & improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a)) ) )
assume that
A1:
right_closed_halfline a c= dom f
and
A2:
right_closed_halfline a c= dom g
and
A3:
f is_+infty_improper_integrable_on a
and
A4:
g is_+infty_improper_integrable_on a
and
A5:
( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = +infty )
and
A6:
( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = -infty )
; ( f - g is_+infty_improper_integrable_on a & improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a)) )
A7:
dom (- g) = dom g
by VALUED_1:8;
A8:
- g is_+infty_improper_integrable_on a
by A2, A4, Th44;
hence
f - g is_+infty_improper_integrable_on a
by A1, A2, A7, A3, A8, A9, Th46; improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a))
improper_integral_+infty ((f - g),a) =
(improper_integral_+infty (f,a)) + (improper_integral_+infty ((- g),a))
by A1, A2, A7, A3, A8, A9, A11, Th46
.=
(improper_integral_+infty (f,a)) + (- (improper_integral_+infty (g,a)))
by A2, A4, Th44
;
hence
improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a))
by XXREAL_3:def 4; verum