0 + (len f) <= n + (len f) by XREAL_1:6;
hence f /^ ((len f) + n) is empty by FINSEQ_5:32; :: thesis: verum