:: deftheorem Def4 defines Sgm0 AFINSQ_2:def 4 :
for X being finite natural-membered set
for b₂ being XFinSequence of NAT holds
( b₂ = Sgm0 X iff ( rng b₂ = X & ( for l, m, k1, k2 being Nat st l < m & m < len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) ) );