let f, g be PartFunc of REAL,REAL; 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; ( 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 )
; ( 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 ( 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 )
;
contradictionthen
- (right_improper_integral (g,a,b)) = - +infty
by A1, A3, A5, Th56, XXREAL_3:6;
hence
contradiction
by A6, A11, XXREAL_3:10;
verum end;
A12:
now ( 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 )
;
contradictionthen
- (right_improper_integral (g,a,b)) = - -infty
by A1, A3, A5, Th56, XXREAL_3:5;
hence
contradiction
by A7, A13, XXREAL_3:10;
verum end;
hence
f - g is_right_improper_integrable_on a,b
by A1, A2, A3, A8, A4, A9, A10, Th58; 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; verum