let n be Nat; :: thesis: the carrier of (product (n --> OrderedNAT)) = Bags n
set X = the carrier of (product (n --> OrderedNAT));
A1: the carrier of (product (n --> OrderedNAT)) = product (Carrier (n --> OrderedNAT)) by YELLOW_1:def 4;

now :: thesis: for x being object holds
( ( x in the carrier of (product (n --> OrderedNAT)) implies x in Bags n ) & ( x in Bags n implies x in the carrier of (product (n --> OrderedNAT)) ) )

let x be object ; :: thesis: ( ( x in the carrier of (product (n --> OrderedNAT)) implies x in Bags n ) & ( x in Bags n implies x in the carrier of (product (n --> OrderedNAT)) ) )

hereby :: thesis: ( x in Bags n implies x in the carrier of (product (n --> OrderedNAT)) )

assume x in the carrier of (product (n --> OrderedNAT)) ; :: thesis: x in Bags n
then consider g being Function such that
A2: x = g and
A3: dom g = dom (Carrier (n --> OrderedNAT)) and
A4: for i being object st i in dom (Carrier (n --> OrderedNAT)) holds
g . i in (Carrier (n --> OrderedNAT)) . i by A1, CARD_3:def 5;
A5: dom g = n by A3, PARTFUN1:def 2;
A6: rng g c= NAT

proof

let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in rng g or z in NAT )
assume z in rng g ; :: thesis: z in NAT
then consider y being object such that
A7: y in dom g and
A8: z = g . y by FUNCT_1:def 3;
A9: z in (Carrier (n --> OrderedNAT)) . y by A3, A4, A7, A8;
ex R being 1-sorted st
( R = (n --> OrderedNAT) . y & (Carrier (n --> OrderedNAT)) . y = the carrier of R ) by A5, A7, PRALG_1:def 15;
hence z in NAT by A5, A7, A9, DICKSON:def 15, FUNCOP_1:7; :: thesis: verum

end;

A10: dom g = dom (Carrier (n --> OrderedNAT)) by A3
.= n by PARTFUN1:def 2 ;
A11: g is natural-valued by A6, VALUED_0:def 6;
g is ManySortedSet of n by A10, PARTFUN1:def 2, RELAT_1:def 18;
hence x in Bags n by A2, A11, PRE_POLY:def 12; :: thesis: verum

end;

assume x in Bags n ; :: thesis: x in the carrier of (product (n --> OrderedNAT))
then reconsider g = x as natural-valued finite-support ManySortedSet of n ;
A12: dom g = n by PARTFUN1:def 2;

now :: thesis: ex g being natural-valued finite-support ManySortedSet of n st
( x = g & dom g = dom (Carrier (n --> OrderedNAT)) & ( for i being object st i in dom (Carrier (n --> OrderedNAT)) holds
g . i in (Carrier (n --> OrderedNAT)) . i ) )

take g = g; :: thesis: ( x = g & dom g = dom (Carrier (n --> OrderedNAT)) & ( for i being object st i in dom (Carrier (n --> OrderedNAT)) holds
g . i in (Carrier (n --> OrderedNAT)) . i ) )
thus x = g ; :: thesis: ( dom g = dom (Carrier (n --> OrderedNAT)) & ( for i being object st i in dom (Carrier (n --> OrderedNAT)) holds
g . i in (Carrier (n --> OrderedNAT)) . i ) )
thus dom g = dom (Carrier (n --> OrderedNAT)) by A12, PARTFUN1:def 2; :: thesis: for i being object st i in dom (Carrier (n --> OrderedNAT)) holds
g . i in (Carrier (n --> OrderedNAT)) . i
let i be object ; :: thesis: ( i in dom (Carrier (n --> OrderedNAT)) implies g . i in (Carrier (n --> OrderedNAT)) . i )
assume i in dom (Carrier (n --> OrderedNAT)) ; :: thesis: g . i in (Carrier (n --> OrderedNAT)) . i
then A13: i in n ;
reconsider ii = i as set by TARSKI:1;
consider R being 1-sorted such that
A14: R = (n --> OrderedNAT) . ii and
A15: (Carrier (n --> OrderedNAT)) . ii = the carrier of R by PRALG_1:def 15, A13;
R = OrderedNAT by A13, A14, FUNCOP_1:7
.= RelStr(# NAT,NATOrd #) by DICKSON:def 15 ;
then g . ii in (Carrier (n --> OrderedNAT)) . ii by A15;
hence g . i in (Carrier (n --> OrderedNAT)) . i ; :: thesis: verum

end;

then x in product (Carrier (n --> OrderedNAT)) by CARD_3:def 5;
hence x in the carrier of (product (n --> OrderedNAT)) by YELLOW_1:def 4; :: thesis: verum

end;

hence the carrier of (product (n --> OrderedNAT)) = Bags n by TARSKI:2; :: thesis: verum