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

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

end;

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

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

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

end;

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