let f be PartFunc of REAL,ExtREAL; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )

thus A = {a} ; :: thesis: ( f is A -measurable & 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; :: thesis: 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 ; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: ( A = {a} & f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )

thus A = {a} ; :: thesis: ( f is A -measurable & f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )

A2: now :: thesis: for r being Real holds A /\ (less_dom (f,r)) in Borel_Sets

hence A3:
f is A -measurable
by MESFUNC1:def 16; :: thesis: ( f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )let r be Real; :: thesis: A /\ (less_dom (f,b_{1})) in Borel_Sets

end;per cases
( a in less_dom (f,r) or not a in less_dom (f,r) )
;

end;

suppose
a in less_dom (f,r)
; :: thesis: A /\ (less_dom (f,b_{1})) in Borel_Sets

then
A /\ (less_dom (f,r)) = A
by ZFMISC_1:46;

hence A /\ (less_dom (f,r)) in Borel_Sets ; :: thesis: verum

end;hence A /\ (less_dom (f,r)) in Borel_Sets ; :: thesis: verum

suppose
not a in less_dom (f,r)
; :: thesis: A /\ (less_dom (f,b_{1})) in Borel_Sets

then
A /\ (less_dom (f,r)) = {}
by XBOOLE_0:def 7, ZFMISC_1:50;

hence A /\ (less_dom (f,r)) in Borel_Sets by MEASURE1:7; :: thesis: verum

end;hence A /\ (less_dom (f,r)) in Borel_Sets by MEASURE1:7; :: thesis: verum

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; :: thesis: 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 ; :: thesis: verum