let f, g be PartFunc of REAL,REAL; :: thesis: ( f a.e.= g, B-Meas implies f a.e.= g, L-Meas )
assume f a.e.= g, B-Meas ; :: thesis: f a.e.= g, L-Meas
then consider E being Element of Borel_Sets such that
A1: ( B-Meas . E = 0 & f | (E `) = g | (E `) ) by LPSPACE1:def 10;
( {} is empty & {} c= REAL ) ;
then reconsider E0 = {} as Element of Borel_Sets by MEASUR12:72;
A2: E = E \/ E0 ;
then reconsider E1 = E as Element of L-Field by MEASURE3:def 3, MEASUR12:73, MEASUR12:def 11;
(COM B-Meas) . E1 = 0 by A1, A2, MEASURE3:def 5, MEASUR12:73;
hence f a.e.= g, L-Meas by A1, LPSPACE1:def 10, MEASUR12:def 12; :: thesis: verum