let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
let S be SigmaField of X; :: thesis: for f being PartFunc of X,REAL
for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
let f be PartFunc of X,REAL; :: thesis: for B, A being Element of S st f is_measurable_on B & A = (dom f) /\ B holds
f | B is_measurable_on A
let B, A be Element of S; :: thesis: ( f is_measurable_on B & A = (dom f) /\ B implies f | B is_measurable_on A )
assume that
A1: f is_measurable_on B and
A2: A = (dom f) /\ B ; :: thesis: f | B is_measurable_on A
A3: R_EAL f is_measurable_on B by A1, Def6;

now

let r be real number ; :: thesis: A /\ (less_dom ((f | B),r)) in S

now

let x be set ; :: thesis: ( x in A /\ (less_dom ((f | B),r)) iff x in B /\ (less_dom (f,r)) )
( x in dom (f | B) & (f | B) . x < R_EAL r iff ( x in (dom f) /\ B & (f | B) . x < R_EAL r ) ) by RELAT_1:61;
then A4: ( x in A & x in less_dom ((f | B),r) iff ( x in B & x in dom f & (f | B) . x < R_EAL r ) ) by A2, MESFUNC1:def 11, XBOOLE_0:def 4;
( x in B & x in dom f implies ( f . x < R_EAL r iff (f | B) . x < R_EAL r ) ) by FUNCT_1:49;
then ( x in A /\ (less_dom ((f | B),r)) iff ( x in B & x in less_dom (f,r) ) ) by A4, MESFUNC1:def 11, XBOOLE_0:def 4;
hence ( x in A /\ (less_dom ((f | B),r)) iff x in B /\ (less_dom (f,r)) ) by XBOOLE_0:def 4; :: thesis: verum

end;

then ( A /\ (less_dom ((f | B),r)) c= B /\ (less_dom (f,r)) & B /\ (less_dom (f,r)) c= A /\ (less_dom ((f | B),r)) ) by TARSKI:def 3;
then A /\ (less_dom ((f | B),r)) = B /\ (less_dom (f,r)) by XBOOLE_0:def 10;
then A /\ (less_dom ((f | B),(R_EAL r))) in S by A3, MESFUNC1:def 16;
hence A /\ (less_dom ((f | B),r)) in S ; :: thesis: verum

end;

hence f | B is_measurable_on A by Th12; :: thesis: verum