let r be Real; :: thesis: for E being Element of L-Field
for f being PartFunc of REAL,ExtREAL st E = {r} holds
f is E -measurable
let E be Element of L-Field ; :: thesis: for f being PartFunc of REAL,ExtREAL st E = {r} holds
f is E -measurable
let f be PartFunc of REAL,ExtREAL; :: thesis: ( E = {r} implies f is E -measurable )
assume A1: E = {r} ; :: thesis: f is E -measurable
for a being Real holds E /\ (less_dom (f,a)) in L-Field

proof

let a be Real; :: thesis: E /\ (less_dom (f,a)) in L-Field
( E /\ (less_dom (f,a)) = {} or E /\ (less_dom (f,a)) = {r} ) by A1, XBOOLE_1:17, ZFMISC_1:33;
hence E /\ (less_dom (f,a)) in L-Field by A1, MEASURE1:7; :: thesis: verum

end;

hence f is E -measurable by MESFUNC1:def 16; :: thesis: verum