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
now :: thesis: for x being object st x in B /\ (less_dom ((f | A),r)) holds
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;
then A4: B /\ (less_dom ((f | A),r)) c= B /\ (less_dom (f,r)) ;
now :: thesis: for x being object st x in B /\ (less_dom (f,r)) holds
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;
then B /\ (less_dom (f,r)) c= B /\ (less_dom ((f | A),r)) ;
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