let S be set ; :: thesis: for X being ManySortedSet of S
for Y being non-empty ManySortedSet of S
for w being ManySortedFunction of X,Y holds rngs w is ManySortedSubset of Y
let X be ManySortedSet of S; :: thesis: for Y being non-empty ManySortedSet of S
for w being ManySortedFunction of X,Y holds rngs w is ManySortedSubset of Y
let Y be non-empty ManySortedSet of S; :: thesis: for w being ManySortedFunction of X,Y holds rngs w is ManySortedSubset of Y
let w be ManySortedFunction of X,Y; :: thesis: rngs w is ManySortedSubset of Y
let x be object ; :: according to PBOOLE:def 2,PBOOLE:def 18 :: thesis: ( not x in S or (rngs w) . x c= Y . x )
assume x in S ; :: thesis: (rngs w) . x c= Y . x
then (rngs w) . x = rng (w . x) by MSSUBFAM:13;
hence (rngs w) . x c= Y . x ; :: thesis: verum