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}

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

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)

then A3:
f " {a} c= eq_dom (f,a)
;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;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

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

x in f " {a}

then
eq_dom (f,a) c= f " {a}
;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;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

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