theorem :: MESFUN14:31

for E1 being Element of Borel_Sets
for E2 being Element of L-Field
for f being PartFunc of REAL,ExtREAL st E1 = E2 & f is E1 -measurable holds
f is E2 -measurable by Th30, MEASUR12:def 11;