:: deftheorem defines sigma NAT_5:def 4 :
for n being natural Number holds sigma n = sigma (1,n);