:: deftheorem Def3 defines Sigma NAT_5:def 3 :
for k being natural Number
for b₂ being sequence of NAT holds
( b₂ = Sigma k iff for n being Nat holds b₂ . n = sigma (k,n) );