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

now :: thesis: for x being object st x in dom f holds
x in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty))

let x be object ; :: thesis: ( x in dom f implies b₁ in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) )
assume A1: x in dom f ; :: thesis: b₁ in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty))

per cases ( f . x in REAL or f . x = +infty or f . x = -infty ) by XXREAL_0:14;

suppose f . x in REAL ; :: thesis: b₁ in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty))

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: verum

end;

suppose f . x = +infty ; :: thesis: b₁ in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty))

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: verum

end;

suppose f . x = -infty ; :: thesis: b₁ in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty))

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: verum

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: for x being object st x in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) holds
x in dom f

let x be object ; :: thesis: ( x in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) implies b₁ in dom f )
assume x in ((eq_dom (f,-infty)) \/ ((great_dom (f,-infty)) /\ (less_dom (f,+infty)))) \/ (eq_dom (f,+infty)) ; :: thesis: b₁ in dom f
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 ( x in eq_dom (f,-infty) or x in (great_dom (f,-infty)) /\ (less_dom (f,+infty)) or x in eq_dom (f,+infty) ) by A6, XBOOLE_0:def 3;

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

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

end;

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

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

end;

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

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

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: verum