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 A1: ( f is_measurable_on B & A = (dom f) /\ B ) ; :: thesis: f | B is_measurable_on A
then A2: R_EAL f is_measurable_on B by 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:90;
then A3: ( 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 A1, MESFUNC1:def 12, 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:72;
then ( x in A /\ (less_dom (f | B),r) iff ( x in B & x in less_dom f,r ) ) by A3, MESFUNC1:def 12, 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 A2, MESFUNC1:def 17;
hence A /\ (less_dom (f | B),r) in S ; :: thesis: verum

end;

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