len a = len- a by EXCHSORT:24;
hence len- a is finite ; :: thesis: verum