f = f ^ {} ;
hence f | (len f) = f ; :: thesis: verum