let S be set ; :: thesis:
let X be countable ManySortedSet of S; :: thesis:
set Y = S --> NAT;
deffunc H₂( object ) -> Enumeration of (X . $1) = the Enumeration of (X . $1);
consider w being ManySortedSet of S such that
A1: for s being object st s in S holds
w . s = H₂(s) from PBOOLE:sch 4();
w is Function-yielding

let x be object ; :: according to FUNCOP_1:def 6 :: thesis:
assume x in dom w ; :: thesis:
then w . x = H₂(x) by A1;
hence w . x is set ; :: thesis:

end;

end;

then reconsider w = w as ManySortedFunction of X,S --> NAT ;
reconsider Z = rngs w as ManySortedSubset of S --> NAT by Th19;
take Z ; :: thesis:
take w ; :: thesis:
thus w is "1-1" :: thesis:

let x be set ; :: according to MSUALG_3:def 2 :: thesis:
let f be Function; :: thesis:
assume x in dom w ; :: thesis:
then w . x = H₂(x) by A1;
hence ( not w . x = f or f is one-to-one ) ; :: thesis:

end;

thus Z = rngs w ; :: thesis:
let x be set ; :: thesis:
assume x in S ; :: thesis:
then ( w . x = H₂(x) & Z . x = rng (w . x) ) by A1, MSSUBFAM:13;
hence ( w . x is Enumeration of (X . x) & Z . x = card (X . x) ) by AOFA_I00:6; :: thesis: