let S be set ; :: thesis: 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) ) ) )
let X be countable ManySortedSet of S; :: thesis: 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) ) ) )
set Y = S --> NAT;
deffunc H2( 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 = H2(s) from PBOOLE:sch 4();
 w is Function-yielding
proof
let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 w or w . x is set )
assume x in dom w ; :: thesis: w . x is set
then w . x = H2(x) by A1;
hence w . x is set ; :: thesis: verum
end;
then reconsider w = w as ManySortedFunction of S ;
w is ManySortedFunction of X,S --> NAT
proof
let x be object ; :: according to PBOOLE:def 15 :: thesis: ( not x in S or w . x is Element of bool [:(X . x),((S --> NAT) . x):] )
assume A2: x in S ; :: thesis: w . x is Element of bool [:(X . x),((S --> NAT) . x):]
A3: card (X . x) c= NAT by CARD_3:def 14;
A4: w . x = H2(x) by A1, A2;
then A5: dom (w . x) = X . x by AOFA_I00:6;
A6: (S --> NAT) . x = NAT by A2, FUNCOP_1:7;
rng (w . x) c= (S --> NAT) . x by A4, A3, A6, AOFA_I00:6;
hence w . x is Element of bool [:(X . x),((S --> NAT) . x):] by A5, FUNCT_2:2; :: thesis: verum
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: ex w being ManySortedFunction of X,S --> NAT st
( w is "1-1" & Z = rngs w & ( for x being set st x in S holds
( w . x is Enumeration of (X . x) & Z . x = card (X . x) ) ) )
take w ; :: thesis: ( w is "1-1" & Z = rngs w & ( for x being set st x in S holds
( w . x is Enumeration of (X . x) & Z . x = card (X . x) ) ) )
thus w is "1-1" :: thesis: ( Z = rngs w & ( for x being set st x in S holds
( w . x is Enumeration of (X . x) & Z . x = card (X . x) ) ) )
proof
let x be set ; :: according to MSUALG_3:def 2 :: thesis: for b1 being set holds
( not x in proj1 w or not w . x = b1 or b1 is one-to-one )
let f be Function; :: thesis: ( not x in proj1 w or not w . x = f or f is one-to-one )
assume x in dom w ; :: thesis: ( not w . x = f or f is one-to-one )
then w . x = H2(x) by A1;
hence ( not w . x = f or f is one-to-one ) ; :: thesis: verum
end;
thus Z = rngs w ; :: thesis: for x being set st x in S holds
( w . x is Enumeration of (X . x) & Z . x = card (X . x) )
let x be set ; :: thesis: ( x in S implies ( w . x is Enumeration of (X . x) & Z . x = card (X . x) ) )
assume x in S ; :: thesis: ( w . x is Enumeration of (X . x) & Z . x = card (X . x) )
then ( w . x = H2(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: verum