let A be array; :: thesis: dom A = (limit- A) \ (base- A)
consider a, b being ordinal number such that
A0: dom A = a \ b by SEG;
A1: limit- A = sup (dom A) by Th005;
A2: base- A = inf (dom A) by Th007;
thus dom A c= (limit- A) \ (base- A) :: according to XBOOLE_0:def 10 :: thesis: (limit- A) \ (base- A) c= dom A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in dom A or x in (limit- A) \ (base- A) )
assume x in dom A ; :: thesis: x in (limit- A) \ (base- A)
then A3: ( base- A c= x & x in limit- A ) by A1, A2, ORDINAL2:14, ORDINAL2:19;
then ( x in base- A implies x in x ) ;
hence x in (limit- A) \ (base- A) by A3, XBOOLE_0:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (limit- A) \ (base- A) or x in dom A )
assume A5: x in (limit- A) \ (base- A) ; :: thesis: x in dom A
then reconsider x = x as Ordinal ;
ex c being ordinal number st
( c in dom A & x c= c ) by A1, A5, ORDINAL2:21;
then ( a = limit- A & b = base- A ) by A0, A1, A2, Th008;
hence x in dom A by A0, A5; :: thesis: verum