theorem Th29: :: INTEGRA7:29

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