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

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