(len f) + n > (len f) + 0 by XREAL_1:6;
then not (len f) + n in dom f by FINSEQ_3:25;
hence f . ((len f) + n) is zero by FUNCT_1:def 2; :: thesis: verum