let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for E being Element of S st f | E = g | E & E c= dom f & E c= dom g & f is E -measurable holds
g is E -measurable
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for E being Element of S st f | E = g | E & E c= dom f & E c= dom g & f is E -measurable holds
g is E -measurable
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,ExtREAL
for E being Element of S st f | E = g | E & E c= dom f & E c= dom g & f is E -measurable holds
g is E -measurable
let f, g be PartFunc of X,ExtREAL; :: thesis: for E being Element of S st f | E = g | E & E c= dom f & E c= dom g & f is E -measurable holds
g is E -measurable
let A be Element of S; :: thesis: ( f | A = g | A & A c= dom f & A c= dom g & f is A -measurable implies g is A -measurable )
assume that
A1: f | A = g | A and
A2: A c= dom f and
A3: A c= dom g and
A4: f is A -measurable ; :: thesis: g is A -measurable

now :: thesis: for r being Real holds A /\ (less_dom (g,r)) in S

let r be Real; :: thesis: A /\ (less_dom (g,r)) in S

now :: thesis: for x being object st x in A /\ (less_dom (f,r)) holds
x in A /\ (less_dom (g,r))

let x be object ; :: thesis: ( x in A /\ (less_dom (f,r)) implies x in A /\ (less_dom (g,r)) )
assume x in A /\ (less_dom (f,r)) ; :: thesis: x in A /\ (less_dom (g,r))
then A5: ( x in A & x in less_dom (f,r) ) by XBOOLE_0:def 4;
then A6: ( x in dom f & f . x < r ) by MESFUNC1:def 11;
f . x = (f | A) . x by A5, FUNCT_1:49;
then f . x = g . x by A1, A5, FUNCT_1:49;
then x in less_dom (g,r) by A3, A5, A6, MESFUNC1:def 11;
hence x in A /\ (less_dom (g,r)) by A5, XBOOLE_0:def 4; :: thesis: verum

end;

then A7: A /\ (less_dom (f,r)) c= A /\ (less_dom (g,r)) ;

now :: thesis: for x being object st x in A /\ (less_dom (g,r)) holds
x in A /\ (less_dom (f,r))

let x be object ; :: thesis: ( x in A /\ (less_dom (g,r)) implies x in A /\ (less_dom (f,r)) )
assume x in A /\ (less_dom (g,r)) ; :: thesis: x in A /\ (less_dom (f,r))
then A8: ( x in A & x in less_dom (g,r) ) by XBOOLE_0:def 4;
then A9: ( x in dom g & g . x < r ) by MESFUNC1:def 11;
g . x = (g | A) . x by A8, FUNCT_1:49;
then g . x = f . x by A1, A8, FUNCT_1:49;
then x in less_dom (f,r) by A2, A8, A9, MESFUNC1:def 11;
hence x in A /\ (less_dom (f,r)) by A8, XBOOLE_0:def 4; :: thesis: verum

end;

then A /\ (less_dom (g,r)) c= A /\ (less_dom (f,r)) ;
then A /\ (less_dom (g,r)) = A /\ (less_dom (f,r)) by A7;
hence A /\ (less_dom (g,r)) in S by A4, MESFUNC1:def 16; :: thesis: verum

end;

hence g is A -measurable by MESFUNC1:def 16; :: thesis: verum