theorem Th3: :: FDIFF_9:3

for x being Real
for n being Nat holds (1 / x) #Z n = 1 / (x #Z n)