let f be array; :: thesis: ( f is 0 -limited iff f is empty )
thus ( f is 0 -limited implies f is empty ) :: thesis: ( f is empty implies f is 0 -limited )

proof

assume sup (dom f) = 0 ; :: according to EXCHSORT:def 3 :: thesis: f is empty
then dom f c= 0 by ORDINAL6:3;
hence f is empty ; :: thesis: verum

end;

assume f is empty ; :: thesis: f is 0 -limited
hence sup (dom f) = 0 by ORDINAL2:18; :: according to EXCHSORT:def 3 :: thesis: verum