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) 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