let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f being PartFunc of X,ExtREAL
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let M be sigma_Measure of S; :: thesis: for f being PartFunc of X,ExtREAL
for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let f be PartFunc of X,ExtREAL; :: thesis: for A, B being Element of S st dom f = A holds
( f is_measurable_on B iff f is_measurable_on A /\ B )
let A, B be Element of S; :: thesis: ( dom f = A implies ( f is_measurable_on B iff f is_measurable_on A /\ B ) )
assume A1: dom f = A ; :: thesis: ( f is_measurable_on B iff f is_measurable_on A /\ B )

A2: now

let r be real number ; :: thesis: A /\ (less_dom (f,(R_EAL r))) = less_dom (f,(R_EAL r))

A3: now

let x be set ; :: thesis: ( x in A /\ (less_dom (f,(R_EAL r))) iff x in less_dom (f,(R_EAL r)) )
( x in A /\ (less_dom (f,(R_EAL r))) iff ( x in A & x in less_dom (f,(R_EAL r)) ) ) by XBOOLE_0:def 4;
hence ( x in A /\ (less_dom (f,(R_EAL r))) iff x in less_dom (f,(R_EAL r)) ) by A1, MESFUNC1:def 11; :: thesis: verum

end;

then A4: less_dom (f,(R_EAL r)) c= A /\ (less_dom (f,(R_EAL r))) by TARSKI:def 3;
A /\ (less_dom (f,(R_EAL r))) c= less_dom (f,(R_EAL r)) by A3, TARSKI:def 3;
hence A /\ (less_dom (f,(R_EAL r))) = less_dom (f,(R_EAL r)) by A4, XBOOLE_0:def 10; :: thesis: verum

end;

hereby :: thesis: ( f is_measurable_on A /\ B implies f is_measurable_on B )

assume A5: f is_measurable_on B ; :: thesis: f is_measurable_on A /\ B

now

let r be real number ; :: thesis: (A /\ B) /\ (less_dom (f,(R_EAL r))) in S
(A /\ B) /\ (less_dom (f,(R_EAL r))) = B /\ (A /\ (less_dom (f,(R_EAL r)))) by XBOOLE_1:16
.= B /\ (less_dom (f,(R_EAL r))) by A2 ;
hence (A /\ B) /\ (less_dom (f,(R_EAL r))) in S by A5, MESFUNC1:def 16; :: thesis: verum

end;

hence f is_measurable_on A /\ B by MESFUNC1:def 16; :: thesis: verum

end;

assume A6: f is_measurable_on A /\ B ; :: thesis: f is_measurable_on B

now

let r be real number ; :: thesis: B /\ (less_dom (f,(R_EAL r))) in S
(A /\ B) /\ (less_dom (f,(R_EAL r))) = B /\ (A /\ (less_dom (f,(R_EAL r)))) by XBOOLE_1:16
.= B /\ (less_dom (f,(R_EAL r))) by A2 ;
hence B /\ (less_dom (f,(R_EAL r))) in S by A6, MESFUNC1:def 16; :: thesis: verum

end;

hence f is_measurable_on B by MESFUNC1:def 16; :: thesis: verum