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

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

let x be object ; :: thesis: ( x in great_eq_dom (f,+infty) implies x in eq_dom (f,+infty) )
assume x in great_eq_dom (f,+infty) ; :: thesis: x in eq_dom (f,+infty)
then A1: ( x in dom f & +infty <= f . x ) by MESFUNC1:def 14;
then f . x = +infty by XXREAL_0:4;
hence x in eq_dom (f,+infty) by A1, MESFUNC1:def 15; :: thesis: verum

end;

then A2: great_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 great_eq_dom (f,+infty)

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

end;

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