A1: len f <> 1 by NAT_D:60;
len f <> 0 by NAT_D:60;
hence not L~ f is empty by A1, TOPREAL1:22; :: thesis: verum