:: deftheorem defines \ NEWTON02:def 1 :
for n being natural number holds n \ = (1,1) In_Power n;