let X be set ; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:

let x be object ; :: thesis:
assume x in great_eq_dom (f,+infty) ; :: thesis:
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:

end;

then A2: great_eq_dom (f,+infty) c= eq_dom (f,+infty) ;

let x be object ; :: thesis:
assume x in eq_dom (f,+infty) ; :: thesis:
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:

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: