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