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

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

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

let f be PartFunc of X,ExtREAL; :: 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 )

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

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

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

let f be PartFunc of X,ExtREAL; :: 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 )

A2: now :: thesis: for r being Real holds A /\ (less_dom (f,r)) = less_dom (f,r)

let r be Real; :: thesis: A /\ (less_dom (f,r)) = less_dom (f,r)

A /\ (less_dom (f,r)) c= less_dom (f,r) by A3;

hence A /\ (less_dom (f,r)) = less_dom (f,r) by A4; :: thesis: verum

end;A3: now :: thesis: for x being object holds

( x in A /\ (less_dom (f,r)) iff x in less_dom (f,r) )

then A4:
less_dom (f,r) c= A /\ (less_dom (f,r))
;( x in A /\ (less_dom (f,r)) iff x in less_dom (f,r) )

let x be object ; :: thesis: ( x in A /\ (less_dom (f,r)) iff x in less_dom (f,r) )

( x in A /\ (less_dom (f,r)) iff ( x in A & x in less_dom (f,r) ) ) by XBOOLE_0:def 4;

hence ( x in A /\ (less_dom (f,r)) iff x in less_dom (f,r) ) by A1, MESFUNC1:def 11; :: thesis: verum

end;( x in A /\ (less_dom (f,r)) iff ( x in A & x in less_dom (f,r) ) ) by XBOOLE_0:def 4;

hence ( x in A /\ (less_dom (f,r)) iff x in less_dom (f,r) ) by A1, MESFUNC1:def 11; :: thesis: verum

A /\ (less_dom (f,r)) c= less_dom (f,r) by A3;

hence A /\ (less_dom (f,r)) = less_dom (f,r) by A4; :: thesis: verum

hereby :: thesis: ( f is A /\ B -measurable implies f is B -measurable )

assume A6:
f is A /\ B -measurable
; :: thesis: f is B -measurable assume A5:
f is B -measurable
; :: thesis: f is A /\ B -measurable

end;now :: thesis: for r being Real holds (A /\ B) /\ (less_dom (f,r)) in S

hence
f is A /\ B -measurable
by MESFUNC1:def 16; :: thesis: verumlet r be Real; :: thesis: (A /\ B) /\ (less_dom (f,r)) in S

(A /\ B) /\ (less_dom (f,r)) = B /\ (A /\ (less_dom (f,r))) by XBOOLE_1:16

.= B /\ (less_dom (f,r)) by A2 ;

hence (A /\ B) /\ (less_dom (f,r)) in S by A5, MESFUNC1:def 16; :: thesis: verum

end;(A /\ B) /\ (less_dom (f,r)) = B /\ (A /\ (less_dom (f,r))) by XBOOLE_1:16

.= B /\ (less_dom (f,r)) by A2 ;

hence (A /\ B) /\ (less_dom (f,r)) in S by A5, MESFUNC1:def 16; :: thesis: verum

now :: thesis: for r being Real holds B /\ (less_dom (f,r)) in S

hence
f is B -measurable
by MESFUNC1:def 16; :: thesis: verumlet r be Real; :: thesis: B /\ (less_dom (f,r)) in S

(A /\ B) /\ (less_dom (f,r)) = B /\ (A /\ (less_dom (f,r))) by XBOOLE_1:16

.= B /\ (less_dom (f,r)) by A2 ;

hence B /\ (less_dom (f,r)) in S by A6, MESFUNC1:def 16; :: thesis: verum

end;(A /\ B) /\ (less_dom (f,r)) = B /\ (A /\ (less_dom (f,r))) by XBOOLE_1:16

.= B /\ (less_dom (f,r)) by A2 ;

hence B /\ (less_dom (f,r)) in S by A6, MESFUNC1:def 16; :: thesis: verum