let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for A being Element of S st f is A -measurable & A c= dom f holds
abs f is A -measurable
let S be SigmaField of X; :: thesis: for f being PartFunc of X,REAL
for A being Element of S st f is A -measurable & A c= dom f holds
abs f is A -measurable
let f be PartFunc of X,REAL; :: thesis: for A being Element of S st f is A -measurable & A c= dom f holds
abs f is A -measurable
let A be Element of S; :: thesis: ( f is A -measurable & A c= dom f implies abs f is A -measurable )
assume that
A1: f is A -measurable and
A2: A c= dom f ; :: thesis: abs f is A -measurable
R_EAL f is A -measurable by A1;
then |.(R_EAL f).| is A -measurable by A2, MESFUNC2:27;
then R_EAL (abs f) is A -measurable by Th44;
hence abs f is A -measurable ; :: thesis: verum