theorem :: EXCHSORT:19

for f being array holds
( f is 0 -limited iff f is empty )