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_measurable_on E
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_measurable_on E
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_measurable_on E
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_measurable_on E
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_measurable_on E )
assume A1: E = dom f ; :: thesis: ( ex x being set st
( x in dom f & not f . x = r ) or f is_measurable_on E )
r in REAL ;
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 set 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_measurable_on E

now

let x be Element of X; :: thesis: ( x in dom (R_EAL f) implies (R_EAL f) . x = g0 . x )
assume A6: x in dom (R_EAL f) ; :: thesis: (R_EAL f) . x = g0 . x
then (R_EAL f) . x = r by A5;
hence (R_EAL f) . x = g0 . x by A1, A4, A6; :: thesis: verum

end;

then g0 = R_EAL f by A1, A3, PARTFUN1:5;
then R_EAL f is_measurable_on E by A2, MESFUNC2:34;
hence f is_measurable_on E by MESFUNC6:def 1; :: thesis: verum