let X be set ; :: thesis: for A being finite 0 -based array of X st A <> {} holds
last A in X
let A be finite 0 -based array of X; :: thesis: ( A <> {} implies last A in X )
assume A <> {} ; :: thesis: last A in X
then consider n being Nat such that
A1: dom A = n + 1 by NAT_1:6;
Segm (n + 1) = succ (Segm n) by NAT_1:38;
then ( n in dom A & union (dom A) = n ) by A1, ORDINAL1:6, ORDINAL2:2;
hence last A in X by FUNCT_1:102; :: thesis: verum