for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for E1 being Element of S
for E2 being Element of COM (S,M)
for f being PartFunc of X,ExtREAL st E1 = E2 & f is E1 -measurable holds
f is E2 -measurable