let f be PartFunc of REAL,ExtREAL; for a being Real st a in dom f holds
ex A being Element of Borel_Sets st
( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )
let a be Real; ( a in dom f implies ex A being Element of Borel_Sets st
( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 ) )
assume A1:
a in dom f
; ex A being Element of Borel_Sets st
( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )
reconsider A = {a} as Element of Borel_Sets by Lm6;
take
A
; ( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )
thus
A = {a}
; ( f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )
hence A3:
f is A -measurable
by MESFUNC1:def 16; ( f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )
A4:
A = (dom f) /\ A
by A1, ZFMISC_1:31, XBOOLE_1:28;
then A5:
f | A is A -measurable
by A2, MESFUNC1:def 16, MESFUNC5:42;
reconsider a1 = a as R_eal by XXREAL_0:def 1;
A6:
( A = [.a,a.] & A = [.a1,a1.] )
by XXREAL_1:17;
then A7: B-Meas . A =
diameter A
by MEASUR12:71
.=
0
by A6, MEASURE5:11
;
A8:
dom (f | A) = A
by A4, RELAT_1:61;
then A9:
( dom (max+ (f | A)) = A & dom (max- (f | A)) = A )
by MESFUNC2:def 2, MESFUNC2:def 3;
A10:
( max+ (f | A) is A -measurable & max- (f | A) is A -measurable )
by A5, A8, MESFUN11:10;
then
Integral (B-Meas,((max+ (f | A)) | A)) = 0
by A7, A9, MESFUNC5:94;
then A11:
integral+ (B-Meas,(max+ (f | A))) < +infty
by A9, A10, MESFUNC5:88, MESFUN11:5;
Integral (B-Meas,((max- (f | A)) | A)) = 0
by A7, A9, A10, MESFUNC5:94;
then
integral+ (B-Meas,(max- (f | A))) = 0
by A9, A10, MESFUNC5:88, MESFUN11:5;
hence
f | A is_integrable_on B-Meas
by A8, A4, A11, A3, MESFUNC5:42, MESFUNC5:def 17; Integral (B-Meas,(f | A)) = 0
Integral (B-Meas,((f | A) | A)) = 0
by A4, A8, A7, A3, MESFUNC5:42, MESFUNC5:94;
hence
Integral (B-Meas,(f | A)) = 0
; verum