:: deftheorem Def4 defines Decomp POLYNOM3:def 4 :
for i being non zero Element of NAT
for n being Element of NAT
for b₃ being FinSequence of i -tuples_on NAT holds
( b₃ = Decomp (n,i) iff ex A being finite Subset of (i -tuples_on NAT) st
( b₃ = SgmX ((TuplesOrder i),A) & ( for p being Element of i -tuples_on NAT holds
( p in A iff Sum p = n ) ) ) );