let x be non empty set ; :: thesis: for M being ManySortedSet of NAT
for s being subsequence of M holds rng s c= rng M
let M be ManySortedSet of NAT ; :: thesis: for s being subsequence of M holds rng s c= rng M
let s be subsequence of M; :: thesis: rng s c= rng M
ex N being increasing sequence of NAT st s = M * N by Def13;
hence rng s c= rng M by RELAT_1:26; :: thesis: verum