1 <= len f by NAT_1:14;
hence len (f | 1) = 1 by Th59; :: thesis: verum