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)

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

hence
f is E2 -measurable
by MESFUNC1:def 16; :: thesis: verum
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;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