let X be non empty set ; :: thesis: for f being PartFunc of X,ExtREAL
for a being R_eal holds eq_dom f,a = f " {a}
let f be PartFunc of X,ExtREAL ; :: thesis: for a being R_eal holds eq_dom f,a = f " {a}
let a be R_eal; :: thesis: eq_dom f,a = f " {a}

now

let x be set ; :: thesis: ( x in eq_dom f,a implies x in f " {a} )
assume x in eq_dom f,a ; :: thesis: x in f " {a}
then A1: ( x in dom f & f . x = a ) by MESFUNC1:def 16;
then f . x in {a} by TARSKI:def 1;
hence x in f " {a} by A1, FUNCT_1:def 13; :: thesis: verum

end;

then A2: eq_dom f,a c= f " {a} by TARSKI:def 3;

now

let x be set ; :: thesis: ( x in f " {a} implies x in eq_dom f,a )
assume x in f " {a} ; :: thesis: x in eq_dom f,a
then A3: ( x in dom f & f . x in {a} ) by FUNCT_1:def 13;
then f . x = a by TARSKI:def 1;
hence x in eq_dom f,a by A3, MESFUNC1:def 16; :: thesis: verum

end;

then f " {a} c= eq_dom f,a by TARSKI:def 3;
hence eq_dom f,a = f " {a} by A2, XBOOLE_0:def 10; :: thesis: verum