:: deftheorem Def13 defines Sgm FINSEQ_1:def 13 :
for X being set st ex k being Nat st X c= Seg k holds
for b₂ being FinSequence of NAT holds
( b₂ = Sgm X iff ( rng b₂ = X & ( for l, m, k1, k2 being Nat st 1 <= l & l < m & m <= len b₂ & k1 = b₂ . l & k2 = b₂ . m holds
k1 < k2 ) ) );