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)

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

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)

then A2:
less_eq_dom (f,-infty) c= eq_dom (f,-infty)
;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;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

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

x in less_eq_dom (f,-infty)

then
eq_dom (f,-infty) c= less_eq_dom (f,-infty)
;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;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

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