let X be non empty set ; :: thesis: 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

let S be SigmaField of X; :: thesis: 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

let M be sigma_Measure of S; :: thesis: 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

let E1 be Element of S; :: thesis: 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

let E2 be Element of COM (S,M); :: thesis: for f being PartFunc of X,ExtREAL st E1 = E2 & f is E1 -measurable holds
f is E2 -measurable

let f be PartFunc of X,ExtREAL; :: thesis: ( E1 = E2 & f is E1 -measurable implies f is E2 -measurable )
assume that
A1: E1 = E2 and
A2: f is E1 -measurable ; :: thesis: f is E2 -measurable
for r being Real holds E2 /\ (less_dom (f,r)) in COM (S,M)
proof
let r be Real; :: thesis: E2 /\ (less_dom (f,r)) in COM (S,M)
E1 /\ (less_dom (f,r)) in S by ;
then E2 /\ (less_dom (f,r)) is Element of COM (S,M) by ;
hence E2 /\ (less_dom (f,r)) in COM (S,M) ; :: thesis: verum
end;
hence f is E2 -measurable by MESFUNC1:def 16; :: thesis: verum