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 A2, MESFUNC1:def 16;
then E2 /\ (less_dom (f,r)) is Element of COM (S,M) by A1, Th27;
hence E2 /\ (less_dom (f,r)) in COM (S,M) ; :: thesis: verum

end;

hence f is E2 -measurable by MESFUNC1:def 16; :: thesis: verum