not a :=len f destroysdestroy intloc 0 by SCMFSA7B:22;
hence a :=len f is good by Def6; :: thesis: verum