let X be non empty set ; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
let a be R_eal; :: thesis:

let x be object ; :: thesis:
assume A1: x in f " {a} ; :: thesis:
then f . x in {a} by FUNCT_1:def 7;
then A2: f . x = a by TARSKI:def 1;
x in dom f by A1, FUNCT_1:def 7;
hence x in eq_dom (f,a) by A2, MESFUNC1:def 15; :: thesis:

end;

then A3: f " {a} c= eq_dom (f,a) ;

let x be object ; :: thesis:
assume A4: x in eq_dom (f,a) ; :: thesis:
then f . x = a by MESFUNC1:def 15;
then A5: f . x in {a} by TARSKI:def 1;
x in dom f by A4, MESFUNC1:def 15;
hence x in f " {a} by A5, FUNCT_1:def 7; :: thesis:

end;

then eq_dom (f,a) c= f " {a} ;
hence eq_dom (f,a) = f " {a} by A3; :: thesis: