theorem Th16: :: RADIX_1:17

for m being Nat
for x being Tuple of 1, INT st x /. 1 = m holds
x = <*m*>