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