let f be PartFunc of REAL,REAL; :: 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 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 )

then a in dom (R_EAL f) by MESFUNC5:def 7;

then consider A being Element of Borel_Sets such that

A1: A = {a} and

A2: R_EAL f is A -measurable and

A3: (R_EAL f) | A is_integrable_on B-Meas and

A4: Integral (B-Meas,((R_EAL f) | A)) = 0 by Th45;

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

thus f is A -measurable by A2, MESFUNC6:def 1; :: thesis: ( f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )

(R_EAL f) | A = f | A by MESFUNC5:def 7;

then (R_EAL f) | A = R_EAL (f | A) by MESFUNC5:def 7;

hence ( f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 ) by A3, A4, MESFUNC6:def 3, MESFUNC6:def 4; :: 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 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 )

then a in dom (R_EAL f) by MESFUNC5:def 7;

then consider A being Element of Borel_Sets such that

A1: A = {a} and

A2: R_EAL f is A -measurable and

A3: (R_EAL f) | A is_integrable_on B-Meas and

A4: Integral (B-Meas,((R_EAL f) | A)) = 0 by Th45;

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

thus f is A -measurable by A2, MESFUNC6:def 1; :: thesis: ( f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 )

(R_EAL f) | A = f | A by MESFUNC5:def 7;

then (R_EAL f) | A = R_EAL (f | A) by MESFUNC5:def 7;

hence ( f | A is_integrable_on B-Meas & Integral (B-Meas,(f | A)) = 0 ) by A3, A4, MESFUNC6:def 3, MESFUNC6:def 4; :: thesis: verum