theorem Th3: :: HFDIFF_1:3

for n being Element of NAT st n >= 1 holds
( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} )