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 B -measurable iff f is A /\ B -measurable )

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 B -measurable iff f is A /\ B -measurable )

let f be PartFunc of X,COMPLEX; :: thesis: for A, B being Element of S st dom f = A holds

( f is B -measurable iff f is A /\ B -measurable )

let A, B be Element of S; :: thesis: ( dom f = A implies ( f is B -measurable iff f is A /\ B -measurable ) )

assume A1: dom f = A ; :: thesis: ( f is B -measurable iff f is A /\ B -measurable )

then A2: dom (Re f) = A by COMSEQ_3:def 3;

A3: dom (Im f) = A by A1, COMSEQ_3:def 4;

hence ( f is B -measurable implies f is A /\ B -measurable ) by A2, MESFUNC6:80; :: thesis: ( f is A /\ B -measurable implies f is B -measurable )

thus ( f is A /\ B -measurable implies f is B -measurable ) by A2, A3, MESFUNC6:80; :: thesis: verum

for f being PartFunc of X,COMPLEX

for A, B being Element of S st dom f = A holds

( f is B -measurable iff f is A /\ B -measurable )

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 B -measurable iff f is A /\ B -measurable )

let f be PartFunc of X,COMPLEX; :: thesis: for A, B being Element of S st dom f = A holds

( f is B -measurable iff f is A /\ B -measurable )

let A, B be Element of S; :: thesis: ( dom f = A implies ( f is B -measurable iff f is A /\ B -measurable ) )

assume A1: dom f = A ; :: thesis: ( f is B -measurable iff f is A /\ B -measurable )

then A2: dom (Re f) = A by COMSEQ_3:def 3;

A3: dom (Im f) = A by A1, COMSEQ_3:def 4;

hence ( f is B -measurable implies f is A /\ B -measurable ) by A2, MESFUNC6:80; :: thesis: ( f is A /\ B -measurable implies f is B -measurable )

thus ( f is A /\ B -measurable implies f is B -measurable ) by A2, A3, MESFUNC6:80; :: thesis: verum