let r be Real; :: thesis: for E being Element of L-Field
for f being PartFunc of REAL,REAL st E = {r} holds
f is E -measurable
let E be Element of L-Field ; :: thesis: for f being PartFunc of REAL,REAL st E = {r} holds
f is E -measurable
let f be PartFunc of REAL,REAL; :: thesis: ( E = {r} implies f is E -measurable )
assume E = {r} ; :: thesis: f is E -measurable
then R_EAL f is E -measurable by Th31;
hence f is E -measurable by MESFUNC6:def 1; :: thesis: verum