let A1 be Element of Borel_Sets ; :: thesis: for A2 being Element of L-Field

for f being PartFunc of REAL,ExtREAL st A1 = A2 & f is A1 -measurable holds

f is A2 -measurable

let A2 be Element of L-Field ; :: thesis: for f being PartFunc of REAL,ExtREAL st A1 = A2 & f is A1 -measurable holds

f is A2 -measurable

let f be PartFunc of REAL,ExtREAL; :: thesis: ( A1 = A2 & f is A1 -measurable implies f is A2 -measurable )

assume that

A1: A1 = A2 and

A2: f is A1 -measurable ; :: thesis: f is A2 -measurable

for r being Real holds A2 /\ (less_dom (f,r)) in L-Field by A1, A2, MESFUNC1:def 16, MEASUR12:75;

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

for f being PartFunc of REAL,ExtREAL st A1 = A2 & f is A1 -measurable holds

f is A2 -measurable

let A2 be Element of L-Field ; :: thesis: for f being PartFunc of REAL,ExtREAL st A1 = A2 & f is A1 -measurable holds

f is A2 -measurable

let f be PartFunc of REAL,ExtREAL; :: thesis: ( A1 = A2 & f is A1 -measurable implies f is A2 -measurable )

assume that

A1: A1 = A2 and

A2: f is A1 -measurable ; :: thesis: f is A2 -measurable

for r being Real holds A2 /\ (less_dom (f,r)) in L-Field by A1, A2, MESFUNC1:def 16, MEASUR12:75;

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