theorem Th23: :: NUMBER16:23

for n being non zero Nat holds 0 in rng (pfexp n)