theorem :: MSAFREE4:20

for S being set
for X being countable ManySortedSet of S ex Y being ManySortedSubset of S --> NAT ex w being ManySortedFunction of X,S --> NAT st
( w is "1-1" & Y = rngs w & ( for x being set st x in S holds
( w . x is Enumeration of (X . x) & Y . x = card (X . x) ) ) )