let a, b be Real; for f being PartFunc of REAL,REAL st ].a,b.[ c= dom f & f is_improper_integrable_on a,b holds
for E being Element of L-Field st E c= ].a,b.[ holds
f is E -measurable
let f be PartFunc of REAL,REAL; ( ].a,b.[ c= dom f & f is_improper_integrable_on a,b implies for E being Element of L-Field st E c= ].a,b.[ holds
f is E -measurable )
assume that
A1:
].a,b.[ c= dom f
and
A2:
f is_improper_integrable_on a,b
; for E being Element of L-Field st E c= ].a,b.[ holds
f is E -measurable
consider c being Real such that
A3:
( a < c & c < b )
and
A4:
f is_left_improper_integrable_on a,c
and
A5:
f is_right_improper_integrable_on c,b
and
( ( not left_improper_integral (f,a,c) = -infty or not right_improper_integral (f,c,b) = +infty ) & ( not left_improper_integral (f,a,c) = +infty or not right_improper_integral (f,c,b) = -infty ) )
by A2, INTEGR24:def 5;
hereby verum
let E be
Element of
L-Field ;
( E c= ].a,b.[ implies f is E -measurable )assume A6:
E c= ].a,b.[
;
f is E -measurable
].a,c.] c= ].a,b.[
by A3, XXREAL_1:49;
then A7:
].a,c.] c= dom f
by A1;
[.c,b.[ c= ].a,b.[
by A3, XXREAL_1:48;
then A8:
[.c,b.[ c= dom f
by A1;
reconsider L =
].a,c.] as
Element of
L-Field by MEASUR10:5, MEASUR12:75;
A9:
f is
E /\ L -measurable
by A7, A4, Th34, XBOOLE_1:17;
reconsider R =
[.c,b.[ as
Element of
L-Field by MEASUR10:5, MEASUR12:75;
A10:
L \/ R = ].a,b.[
by A3, XXREAL_1:172;
A11:
(E /\ L) \/ (E /\ R) =
E /\ (L \/ R)
by XBOOLE_1:23
.=
E
by A6, A10, XBOOLE_1:28
;
f is
E /\ R -measurable
by A8, A5, Th33, XBOOLE_1:17;
hence
f is
E -measurable
by A11, A9, MESFUNC6:17;
verum
end;