let X be non empty set ; :: thesis: for S being SigmaField of X

for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL holds

( f | A is A -measurable iff f is A -measurable )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL holds

( f | A is A -measurable iff f is A -measurable )

let M be sigma_Measure of S; :: thesis: for A being Element of S

for f being PartFunc of X,ExtREAL holds

( f | A is A -measurable iff f is A -measurable )

let A be Element of S; :: thesis: for f being PartFunc of X,ExtREAL holds

( f | A is A -measurable iff f is A -measurable )

let f be PartFunc of X,ExtREAL; :: thesis: ( f | A is A -measurable iff f is A -measurable )

assume A2: f is A -measurable ; :: thesis: f | A is A -measurable

for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL holds

( f | A is A -measurable iff f is A -measurable )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S

for A being Element of S

for f being PartFunc of X,ExtREAL holds

( f | A is A -measurable iff f is A -measurable )

let M be sigma_Measure of S; :: thesis: for A being Element of S

for f being PartFunc of X,ExtREAL holds

( f | A is A -measurable iff f is A -measurable )

let A be Element of S; :: thesis: for f being PartFunc of X,ExtREAL holds

( f | A is A -measurable iff f is A -measurable )

let f be PartFunc of X,ExtREAL; :: thesis: ( f | A is A -measurable iff f is A -measurable )

now :: thesis: ( f | A is A -measurable implies f is A -measurable )

hence
( f | A is A -measurable implies f is A -measurable )
; :: thesis: ( f is A -measurable implies f | A is A -measurable )assume A1:
f | A is A -measurable
; :: thesis: f is A -measurable

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

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

A /\ (less_dom ((f | A),r)) in S by A1, MESFUNC1:def 16;

then A /\ (A /\ (less_dom (f,r))) in S by Lm5;

then (A /\ A) /\ (less_dom (f,r)) in S by XBOOLE_1:16;

hence A /\ (less_dom (f,r)) in S ; :: thesis: verum

end;A /\ (less_dom ((f | A),r)) in S by A1, MESFUNC1:def 16;

then A /\ (A /\ (less_dom (f,r))) in S by Lm5;

then (A /\ A) /\ (less_dom (f,r)) in S by XBOOLE_1:16;

hence A /\ (less_dom (f,r)) in S ; :: thesis: verum

assume A2: f is A -measurable ; :: thesis: f | A is A -measurable

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

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

(A /\ A) /\ (less_dom (f,r)) in S by A2, MESFUNC1:def 16;

then A /\ (A /\ (less_dom (f,r))) in S by XBOOLE_1:16;

hence A /\ (less_dom ((f | A),r)) in S by Lm5; :: thesis: verum

end;(A /\ A) /\ (less_dom (f,r)) in S by A2, MESFUNC1:def 16;

then A /\ (A /\ (less_dom (f,r))) in S by XBOOLE_1:16;

hence A /\ (less_dom ((f | A),r)) in S by Lm5; :: thesis: verum