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