let s be ManySortedSet of NAT ; :: thesis: for k being Nat holds rng (s ^\ k) c= rng s
let k be Nat; :: thesis: rng (s ^\ k) c= rng s
let i be set ; :: according to TARSKI:def 3 :: thesis: ( not i in rng (s ^\ k) or i in rng s )
assume i in rng (s ^\ k) ; :: thesis: i in rng s
then consider u being set such that
W1: u in dom (s ^\ k) and
W2: i = (s ^\ k) . u by FUNCT_1:def 3;
reconsider n = u as Element of NAT by W1, PARTFUN1:def 2;
X: dom s = NAT by PARTFUN1:def 2;
i = s . (n + k) by W2, Def3;
hence i in rng s by X, FUNCT_1:3; :: thesis: verum