let n be Element of 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

let x be set ; :: 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 set 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 4;

now

rng g c= NAT

proof

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

end;

hence g is natural-valued by VALUED_0:def 6; :: thesis: ( g is finite-support & g is ManySortedSet of )
support g is finite by A5, FINSET_1:13, POLYNOM1:41;
hence g is finite-support by POLYNOM1:def 8; :: thesis: g is ManySortedSet of
dom g = dom (Carrier (n --> OrderedNAT )) by A3
.= n by PARTFUN1:def 4 ;
hence g is ManySortedSet of by PARTFUN1:def 4, RELAT_1:def 18; :: thesis: verum

end;

hence x in Bags n by A2, POLYNOM1:def 14; :: 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 by POLYNOM1:def 14;
A11: dom g = n by PARTFUN1:def 4;

now

take g = g; :: thesis: ( x = g & dom g = dom (Carrier (n --> OrderedNAT )) & ( for i being set 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 set st i in dom (Carrier (n --> OrderedNAT )) holds
g . i in (Carrier (n --> OrderedNAT )) . i ) )
thus dom g = dom (Carrier (n --> OrderedNAT )) by A11, PARTFUN1:def 4; :: thesis: for i being set st i in dom (Carrier (n --> OrderedNAT )) holds
g . i in (Carrier (n --> OrderedNAT )) . i
let i be set ; :: thesis: ( i in dom (Carrier (n --> OrderedNAT )) implies g . i in (Carrier (n --> OrderedNAT )) . i )
assume A12: i in dom (Carrier (n --> OrderedNAT )) ; :: thesis: g . i in (Carrier (n --> OrderedNAT )) . i
A13: i in n by A12, PARTFUN1:def 4;
then consider R being 1-sorted such that
A14: R = (n --> OrderedNAT ) . i and
A15: (Carrier (n --> OrderedNAT )) . i = the carrier of R by PRALG_1:def 13;
R = OrderedNAT by A13, A14, FUNCOP_1:13;
hence g . i in (Carrier (n --> OrderedNAT )) . i by A15, DICKSON:def 15; :: 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