let s be ManySortedSet of NAT ; :: thesis: for k being natural Number holds rng (s ^\ k) c= rng s
let k be natural Number ; :: thesis: rng (s ^\ k) c= rng s
let i be object ; :: 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 object such that
A1: u in dom (s ^\ k) and
A2: i = (s ^\ k) . u by FUNCT_1:def 3;
reconsider n = u as Element of NAT by A1, PARTFUN1:def 2;
A3: dom s = NAT by PARTFUN1:def 2;
i = s . (n + k) by A2, Def2;
hence i in rng s by A3, FUNCT_1:3, ORDINAL1:def 12; :: thesis: verum