theorem Th3: :: NAT_3:3

for a, n being Nat st a <> 0 holds
n divides n |^ a