let X be set ; :: thesis:
let f be PartFunc of X,ExtREAL; :: thesis:
set A1 = eq_dom (f,-infty);
set A2 = (great_dom (f,-infty)) /\ (less_dom (f,+infty));
set A3 = eq_dom (f,+infty);

now :: thesis:

let x be object ; :: thesis:
assume A1: x in dom f ; :: thesis:

per cases by XXREAL_0:14;

suppose f . x in REAL ; :: thesis:

then ( f . x > -infty & f . x < +infty ) by XXREAL_0:9, XXREAL_0:12;
then ( x in great_dom (f,-infty) & x in less_dom (f,+infty) ) by A1, MESFUNC1:def 11, MESFUNC1:def 13;
then A2: x in (great_dom (f,-infty)) /\ (less_dom (f,+infty)) by XBOOLE_0:def 4;
( (great_dom (f,-infty)) /\ (less_dom (f,+infty)) c= (eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty))) & (eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty))) c= ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) ) by XBOOLE_1:7;
hence x in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) by A2; :: thesis:

end;

suppose f . x = +infty ; :: thesis:

then A3: x in eq_dom (f,+infty) by A1, MESFUNC1:def 15;
eq_dom (f,+infty) c= ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) by XBOOLE_1:7;
hence x in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) by A3; :: thesis:

end;

suppose f . x = -infty ; :: thesis:

then A4: x in eq_dom (f,-infty) by A1, MESFUNC1:def 15;
( eq_dom (f,-infty) c= (eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty))) & (eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty))) c= ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) ) by XBOOLE_1:7;
hence x in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) by A4; :: thesis:

end;

end;

end;

then A5: dom f c= ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) ;

now :: thesis:

let x be object ; :: thesis:
assume x in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) ; :: thesis:
then A6: ( x in (eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty))) or x in eq_dom (f,+infty) ) by XBOOLE_0:def 3;

per cases by A6, XBOOLE_0:def 3;

suppose x in eq_dom (f,-infty) ; :: thesis:

hence x in dom f by MESFUNC1:def 15; :: thesis:

end;

suppose x in (great_dom (f,-infty)) /\ (less_dom (f,+infty)) ; :: thesis:

then x in great_dom (f,-infty) by XBOOLE_0:def 4;
hence x in dom f by MESFUNC1:def 13; :: thesis:

end;

suppose x in eq_dom (f,+infty) ; :: thesis:

hence x in dom f by MESFUNC1:def 15; :: thesis:

end;

end;

end;

then ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) c= dom f ;
hence dom f = ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) by A5; :: thesis: