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_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; ( 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 )
; ( 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 ( 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 )
;
contradictionthen
- (left_improper_integral (g,a,b)) = - +infty
by A1, A3, A5, Th55, XXREAL_3:6;
hence
contradiction
by A6, A11, XXREAL_3:10;
verum end;
A12:
now ( 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 )
;
contradictionthen
- (left_improper_integral (g,a,b)) = - -infty
by A1, A3, A5, Th55, XXREAL_3:5;
hence
contradiction
by A7, A13, XXREAL_3:10;
verum end;
hence
f - g is_left_improper_integrable_on a,b
by A1, A2, A3, A8, A4, A9, A10, Th57; 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; verum