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 holds
max+ 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 holds
max+ f is A -measurable
let f be PartFunc of X,REAL; :: thesis: for A being Element of S st f is A -measurable holds
max+ f is A -measurable
let A be Element of S; :: thesis: ( f is A -measurable implies max+ f is A -measurable )
assume f is A -measurable ; :: thesis: max+ f is A -measurable
then R_EAL f is A -measurable ;
then max+ (R_EAL f) is A -measurable by MESFUNC2:25;
then R_EAL (max+ f) is A -measurable by Th30;
hence max+ f is A -measurable ; :: thesis: verum