let X be non empty set ; :: thesis: for S being SigmaField of X

for A, B being Element of S

for f being PartFunc of X,ExtREAL st B c= A & f | A is B -measurable holds

f is B -measurable

let S be SigmaField of X; :: thesis: for A, B being Element of S

for f being PartFunc of X,ExtREAL st B c= A & f | A is B -measurable holds

f is B -measurable

let A, B be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st B c= A & f | A is B -measurable holds

f is B -measurable

let f be PartFunc of X,ExtREAL; :: thesis: ( B c= A & f | A is B -measurable implies f is B -measurable )

assume that

A1: B c= A and

A2: f | A is B -measurable ; :: thesis: f is B -measurable

let r be Real; :: according to MESFUNC1:def 15 :: thesis: B /\ (less_dom (f,r)) in S

then B /\ (less_dom ((f | A),r)) = B /\ (less_dom (f,r)) by A4;

hence B /\ (less_dom (f,r)) in S by A2; :: thesis: verum

for A, B being Element of S

for f being PartFunc of X,ExtREAL st B c= A & f | A is B -measurable holds

f is B -measurable

let S be SigmaField of X; :: thesis: for A, B being Element of S

for f being PartFunc of X,ExtREAL st B c= A & f | A is B -measurable holds

f is B -measurable

let A, B be Element of S; :: thesis: for f being PartFunc of X,ExtREAL st B c= A & f | A is B -measurable holds

f is B -measurable

let f be PartFunc of X,ExtREAL; :: thesis: ( B c= A & f | A is B -measurable implies f is B -measurable )

assume that

A1: B c= A and

A2: f | A is B -measurable ; :: thesis: f is B -measurable

let r be Real; :: according to MESFUNC1:def 15 :: thesis: B /\ (less_dom (f,r)) in S

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

x in B /\ (less_dom (f,r))

then A4:
B /\ (less_dom ((f | A),r)) c= B /\ (less_dom (f,r))
;x in B /\ (less_dom (f,r))

let x be object ; :: thesis: ( x in B /\ (less_dom ((f | A),r)) implies x in B /\ (less_dom (f,r)) )

assume x in B /\ (less_dom ((f | A),r)) ; :: thesis: x in B /\ (less_dom (f,r))

then A3: ( x in B & x in less_dom ((f | A),r) ) by XBOOLE_0:def 4;

then ( x in dom (f | A) & (f | A) . x < r ) by MESFUNC1:def 11;

then ( x in dom f & f . x < r ) by RELAT_1:57, FUNCT_1:47;

then x in less_dom (f,r) by MESFUNC1:def 11;

hence x in B /\ (less_dom (f,r)) by A3, XBOOLE_0:def 4; :: thesis: verum

end;assume x in B /\ (less_dom ((f | A),r)) ; :: thesis: x in B /\ (less_dom (f,r))

then A3: ( x in B & x in less_dom ((f | A),r) ) by XBOOLE_0:def 4;

then ( x in dom (f | A) & (f | A) . x < r ) by MESFUNC1:def 11;

then ( x in dom f & f . x < r ) by RELAT_1:57, FUNCT_1:47;

then x in less_dom (f,r) by MESFUNC1:def 11;

hence x in B /\ (less_dom (f,r)) by A3, XBOOLE_0:def 4; :: thesis: verum

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

x in B /\ (less_dom ((f | A),r))

then
B /\ (less_dom (f,r)) c= B /\ (less_dom ((f | A),r))
;x in B /\ (less_dom ((f | A),r))

let x be object ; :: thesis: ( x in B /\ (less_dom (f,r)) implies x in B /\ (less_dom ((f | A),r)) )

assume x in B /\ (less_dom (f,r)) ; :: thesis: x in B /\ (less_dom ((f | A),r))

then A5: ( x in B & x in less_dom (f,r) ) by XBOOLE_0:def 4;

then ( x in dom f & f . x < r ) by MESFUNC1:def 11;

then ( x in dom (f | A) & (f | A) . x < r ) by A1, A5, RELAT_1:57, FUNCT_1:49;

then x in less_dom ((f | A),r) by MESFUNC1:def 11;

hence x in B /\ (less_dom ((f | A),r)) by A5, XBOOLE_0:def 4; :: thesis: verum

end;assume x in B /\ (less_dom (f,r)) ; :: thesis: x in B /\ (less_dom ((f | A),r))

then A5: ( x in B & x in less_dom (f,r) ) by XBOOLE_0:def 4;

then ( x in dom f & f . x < r ) by MESFUNC1:def 11;

then ( x in dom (f | A) & (f | A) . x < r ) by A1, A5, RELAT_1:57, FUNCT_1:49;

then x in less_dom ((f | A),r) by MESFUNC1:def 11;

hence x in B /\ (less_dom ((f | A),r)) by A5, XBOOLE_0:def 4; :: thesis: verum

then B /\ (less_dom ((f | A),r)) = B /\ (less_dom (f,r)) by A4;

hence B /\ (less_dom (f,r)) in S by A2; :: thesis: verum