:: deftheorem Def2 defines sigma NAT_5:def 2 :
for k, n being natural Number
for b₃ being Element of NAT holds
( ( n <> 0 implies ( b₃ = sigma (k,n) iff for m being non zero Nat st n = m holds
b₃ = Sum ((EXP k) | (NatDivisors m)) ) ) & ( not n <> 0 implies ( b₃ = sigma (k,n) iff b₃ = 0 ) ) );