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