theorem :: NAT_1:15

for i, j being natural Number st i * j = 1 holds
i = 1