for n being Nat holds invNAT . n = 1 / (n + 0) by DefRec;
hence lim invNAT = 0 by SEQ_4:31; :: thesis: verum