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 :: thesis: for x being object st x in f " {a} holds
x in eq_dom (f,a)

let x be object ; :: thesis: ( x in f " {a} implies x in eq_dom (f,a) )
assume A1: x in f " {a} ; :: thesis: x in eq_dom (f,a)
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: verum

end;

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

now :: thesis: for x being object st x in eq_dom (f,a) holds
x in f " {a}

let x be object ; :: thesis: ( x in eq_dom (f,a) implies x in f " {a} )
assume A4: x in eq_dom (f,a) ; :: thesis: x in f " {a}
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: verum

end;

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