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 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 ;
then A5: f | A is A -measurable by ;
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 ;
A8: dom (f | A) = A by ;
then A9: ( dom (max+ (f | A)) = A & dom (max- (f | A)) = A ) by ;
A10: ( max+ (f | A) is A -measurable & max- (f | A) is A -measurable ) by ;
then Integral (B-Meas,((max+ (f | A)) | A)) = 0 by ;
then A11: integral+ (B-Meas,(max+ (f | A))) < +infty by ;
Integral (B-Meas,((max- (f | A)) | A)) = 0 by ;
then integral+ (B-Meas,(max- (f | A))) = 0 by ;
hence f | A is_integrable_on B-Meas by ; :: thesis: Integral (B-Meas,(f | A)) = 0
Integral (B-Meas,((f | A) | A)) = 0 by ;
hence Integral (B-Meas,(f | A)) = 0 ; :: thesis: verum