let a, b be ordinal number ; :: thesis: for A being array st dom A = a \ b & not A is empty holds
( base- A = b & limit- A = a )
let A be array; :: thesis: ( dom A = a \ b & not A is empty implies ( base- A = b & limit- A = a ) )
assume A0: ( dom A = a \ b & not A is empty ) ; :: thesis: ( base- A = b & limit- A = a )
set x = the Element of dom A;
dom A <> {} by A0;
then A1: the Element of dom A in a \ b by A0;
( b c= the Element of dom A & the Element of dom A in a ) by A0, ORDINAL6:5;
then A2: ( b in a & b nin b ) by ORDINAL1:12;
then b in a \ b by XBOOLE_0:def 5;
then A5: b in sup (dom A) by A0, ORDINAL2:19;
A is b -based

proof

let c be ordinal number ; :: according to EXCHSORT:def 2 :: thesis: ( c in proj1 A implies ( b in proj1 A & b c= c ) )
thus ( c in proj1 A implies ( b in proj1 A & b c= c ) ) by A0, A2, ORDINAL6:5; :: thesis: verum

end;

hence base- A = b by BA, A0, A1; :: thesis: limit- A = a
A3: a c= sup (dom A)

proof

let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in a or x in sup (dom A) )
assume A4: x in a ; :: thesis: x in sup (dom A)

per cases ( x in b or x nin b ) ;

suppose x in b ; :: thesis: x in sup (dom A)

hence x in sup (dom A) by A5, ORDINAL1:10; :: thesis: verum

end;

suppose x nin b ; :: thesis: x in sup (dom A)

then x in a \ b by A4, XBOOLE_0:def 5;
hence x in sup (dom A) by A0, ORDINAL2:19; :: thesis: verum

end;

end;

end;

sup (dom A) c= sup a by A0, ORDINAL2:22;
then sup (dom A) c= a by ORDINAL2:18;
then a = sup (dom A) by A3, XBOOLE_0:def 10;
hence limit- A = a by Th005; :: thesis: verum