let r be Real; :: thesis: for X being non empty set
for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is E -measurable
let X be non empty set ; :: thesis: for S being SigmaField of X
for E being Element of S
for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is E -measurable
let S be SigmaField of X; :: thesis: for E being Element of S
for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is E -measurable
let E be Element of S; :: thesis: for f being PartFunc of X,REAL st E = dom f & ( for x being set st x in dom f holds
f . x = r ) holds
f is E -measurable
let f be PartFunc of X,REAL; :: thesis: ( E = dom f & ( for x being set st x in dom f holds
f . x = r ) implies f is E -measurable )
assume A1: E = dom f ; :: thesis: ( ex x being set st
( x in dom f & not f . x = r ) or f is E -measurable )
r in REAL by XREAL_0:def 1;
then reconsider r0 = r as R_eal by NUMBERS:31;
set g = R_EAL f;
consider g0 being PartFunc of X,ExtREAL such that
A2: g0 is_simple_func_in S and
A3: dom g0 = E and
A4: for x being object st x in E holds
g0 . x = r0 by MESFUNC5:41;
assume A5: for x being set st x in dom f holds
f . x = r ; :: thesis: f is E -measurable
then g0 = R_EAL f by A1, A3, PARTFUN1:5;
then R_EAL f is E -measurable by A2, MESFUNC2:34;
hence f is E -measurable ; :: thesis: verum