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 )

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

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

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

let 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;

hence f is A -measurable by MESFUNC1:def 16; :: thesis: verum

end;

hence ( f | A is A -measurable implies f is A -measurable ) ; :: thesis: ( f is A -measurable implies f | A is A -measurable )
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

let 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;

hence f | A is A -measurable by MESFUNC1:def 16; :: thesis: verum