let X be non empty set ; 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; 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; 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; ( dom f = A implies ( f is B -measurable iff f is A /\ B -measurable ) )
assume A1:
dom f = A
; ( 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; ( 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; verum