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_measurable_on A iff f is_measurable_on A )
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_measurable_on A iff f is_measurable_on A )
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_measurable_on A iff f is_measurable_on A )
let A be Element of S; :: thesis: for f being PartFunc of X,ExtREAL holds
( f | A is_measurable_on A iff f is_measurable_on A )
let f be PartFunc of X,ExtREAL ; :: thesis: ( f | A is_measurable_on A iff f is_measurable_on A )

now

assume A1: f | A is_measurable_on A ; :: thesis: f is_measurable_on A

now

let r be real number ; :: thesis: A /\ (less_dom f,(R_EAL r)) in S
A /\ (less_dom (f | A),(R_EAL r)) in S by A1, MESFUNC1:def 17;
then A /\ (A /\ (less_dom f,(R_EAL r))) in S by Lm5;
then (A /\ A) /\ (less_dom f,(R_EAL r)) in S by XBOOLE_1:16;
hence A /\ (less_dom f,(R_EAL r)) in S ; :: thesis: verum

end;

hence f is_measurable_on A by MESFUNC1:def 17; :: thesis: verum

end;

hence ( f | A is_measurable_on A implies f is_measurable_on A ) ; :: thesis: ( f is_measurable_on A implies f | A is_measurable_on A )
assume A2: f is_measurable_on A ; :: thesis: f | A is_measurable_on A

now

let r be real number ; :: thesis: A /\ (less_dom (f | A),(R_EAL r)) in S
(A /\ A) /\ (less_dom f,(R_EAL r)) in S by A2, MESFUNC1:def 17;
then A /\ (A /\ (less_dom f,(R_EAL r))) in S by XBOOLE_1:16;
hence A /\ (less_dom (f | A),(R_EAL r)) in S by Lm5; :: thesis: verum

end;

hence f | A is_measurable_on A by MESFUNC1:def 17; :: thesis: verum