for n being Element of NAT holds #Z (n + 1) is_integral_of (n + 1) (#) (#Z n), REAL