A1: len f <> 1 by REALSET1:13;
len f <> 0 by REALSET1:13;
hence not L~ f is empty by A1, TOPREAL1:28; :: thesis: verum