:: deftheorem Def13 defines Sgm FINSEQ_1:def 14 :
for X being set st X is included_in_Seg holds
for b₂ being FinSequence of NAT holds
( b₂ = Sgm X iff ( rng b₂ = X & ( for m, n being Nat st 1 <= m & m < n & n <= len b₂ holds
b₂ . m < b₂ . n ) ) );