theorem Th1: :: NUMPOLY1:1

for n, a being non zero Nat holds 1 <= a * n