(len f) + n >= (len f) + 0 by XREAL_1:6;
hence f | ((len f) + n) = f by AFINSQ_1:52; :: thesis: verum