let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX
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 f being PartFunc of X,COMPLEX
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,COMPLEX; :: 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 )
then A2: dom (Re f) = A by COMSEQ_3:def 3;
A3: dom (Im f) = A by A1, COMSEQ_3:def 4;

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

assume A4: f is_measurable_on B ; :: thesis: f is_measurable_on A /\ B
then Im f is_measurable_on B by Def3;
then A5: Im f is_measurable_on A /\ B by A3, MESFUNC6:80;
Re f is_measurable_on B by A4, Def3;
then Re f is_measurable_on A /\ B by A2, MESFUNC6:80;
hence f is_measurable_on A /\ B by A5, Def3; :: thesis: verum

end;

hereby :: thesis: verum

assume A6: f is_measurable_on A /\ B ; :: thesis: f is_measurable_on B
then Im f is_measurable_on A /\ B by Def3;
then A7: Im f is_measurable_on B by A3, MESFUNC6:80;
Re f is_measurable_on A /\ B by A6, Def3;
then Re f is_measurable_on B by A2, MESFUNC6:80;
hence f is_measurable_on B by A7, Def3; :: thesis: verum

end;