(f | (max ((len f),n))) /^ (max ((len f),n)) is empty ;
hence f /^ (max ((len f),n)) is empty ; :: thesis: verum