let X be non empty set ; :: thesis: for f being PartFunc of X,REAL
for r being Real holds eq_dom f,r = f " {r}
let f be PartFunc of X,REAL ; :: thesis: for r being Real holds eq_dom f,r = f " {r}
let r be Real; :: thesis: eq_dom f,r = f " {r}

now

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

end;

then A3: eq_dom f,r c= f " {r} by TARSKI:def 3;

now

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

end;

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