let a, b be Ordinal; :: 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 A1: ( 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 A1;
then A2: the Element of dom A in a \ b by A1;
A: ( b c= the Element of dom A & the Element of dom A in a ) by A1, ORDINAL6:5;
not b in b ;
then A3: ( b in a & b nin b ) by A, ORDINAL1:12;
then b in a \ b by XBOOLE_0:def 5;
then A4: b in sup (dom A) by A1, ORDINAL2:19;
A is b -based by A1, A3, ORDINAL6:5;
hence base- A = b by Def4, A1, A2; :: thesis: limit- A = a
A5: 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 A6: 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 A4, ORDINAL1:10; :: thesis: verum

end;

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

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

end;

end;

end;

sup (dom A) c= sup a by A1, ORDINAL2:22;
then sup (dom A) c= a by ORDINAL2:18;
then a = sup (dom A) by A5;
hence limit- A = a by Th16; :: thesis: verum