:: deftheorem Def3 defines a_partition EULRPART:def 3 :
for n being Nat
for b₂ being non-zero natural-valued non-decreasing FinSequence holds
( b₂ is a_partition of n iff Sum b₂ = n );