let A be array; :: thesis: dom A = (limit- A) \ (base- A)
consider a, b being Ordinal such that
A1: dom A = a \ b by Def1;
A2: limit- A = sup (dom A) by Th16;
A3: base- A = inf (dom A) by Th20;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom A or x in (limit- A) \ (base- A) )
reconsider xx = x as set by TARSKI:1;
assume x in dom A ; :: thesis: x in (limit- A) \ (base- A)
then A4: ( base- A c= xx & x in limit- A ) by A2, A3, ORDINAL2:14, ORDINAL2:19;
then A: ( x in base- A implies x in xx ) ;
not xx in xx ;
hence x in (limit- A) \ (base- A) by A, A4, XBOOLE_0:def 5; :: thesis: verum
end;
let x be object ; :: 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 st
( c in dom A & x c= c ) by A2, A5, ORDINAL2:21;
then ( a = limit- A & b = base- A ) by A1, A2, A3, Th6;
hence x in dom A by A1, A5; :: thesis: verum