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 )

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

let r be Real; :: thesis: A /\ (less_dom (f,b₁)) in Borel_Sets

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

suppose a in less_dom (f,r) ; :: thesis: A /\ (less_dom (f,b₁)) 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;

suppose not a in less_dom (f,r) ; :: thesis: A /\ (less_dom (f,b₁)) 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;

end;

end;

hence A3: f is A -measurable by MESFUNC1:def 16; :: thesis: ( 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