let X be set ; :: thesis: for f being PartFunc of X,ExtREAL holds less_eq_dom (f,-infty) = eq_dom (f,-infty)
let f be PartFunc of X,ExtREAL; :: thesis: less_eq_dom (f,-infty) = eq_dom (f,-infty)

now :: thesis: for x being object st x in less_eq_dom (f,-infty) holds
x in eq_dom (f,-infty)

let x be object ; :: thesis: ( x in less_eq_dom (f,-infty) implies x in eq_dom (f,-infty) )
assume x in less_eq_dom (f,-infty) ; :: thesis: x in eq_dom (f,-infty)
then A1: ( x in dom f & -infty >= f . x ) by MESFUNC1:def 12;
then f . x = -infty by XXREAL_0:6;
hence x in eq_dom (f,-infty) by A1, MESFUNC1:def 15; :: thesis: verum

end;

then A2: less_eq_dom (f,-infty) c= eq_dom (f,-infty) ;

now :: thesis: for x being object st x in eq_dom (f,-infty) holds
x in less_eq_dom (f,-infty)

let x be object ; :: thesis: ( x in eq_dom (f,-infty) implies x in less_eq_dom (f,-infty) )
assume x in eq_dom (f,-infty) ; :: thesis: x in less_eq_dom (f,-infty)
then ( x in dom f & -infty = f . x ) by MESFUNC1:def 15;
hence x in less_eq_dom (f,-infty) by MESFUNC1:def 12; :: thesis: verum

end;

then eq_dom (f,-infty) c= less_eq_dom (f,-infty) ;
hence less_eq_dom (f,-infty) = eq_dom (f,-infty) by A2; :: thesis: verum