:: deftheorem Def13 defines subsequence VALUED_0:def 17 :
for s, b₂ being ManySortedSet of NAT holds
( b₂ is subsequence of s iff ex N being increasing sequence of NAT st b₂ = s * N );