let n be Nat; :: thesis: the carrier of (product ()) = Bags n
set X = the carrier of (product ());
A1: the carrier of (product ()) = product (Carrier ()) by YELLOW_1:def 4;
now :: thesis: for x being object holds
( ( x in the carrier of (product ()) implies x in Bags n ) & ( x in Bags n implies x in the carrier of (product ()) ) )
let x be object ; :: thesis: ( ( x in the carrier of (product ()) implies x in Bags n ) & ( x in Bags n implies x in the carrier of (product ()) ) )
hereby :: thesis: ( x in Bags n implies x in the carrier of (product ()) )
assume x in the carrier of (product ()) ; :: thesis: x in Bags n
then consider g being Function such that
A2: x = g and
A3: dom g = dom (Carrier ()) and
A4: for i being object st i in dom (Carrier ()) holds
g . i in (Carrier ()) . i by ;
A5: dom g = n by ;
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:
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 ()) . y by A3, A4, A7, A8;
ex R being 1-sorted st
( R = () . y & (Carrier ()) . y = the carrier of R ) by ;
hence z in NAT by ; :: thesis: verum
end;
A10: dom g = dom (Carrier ()) by A3
.= n by PARTFUN1:def 2 ;
A11: g is natural-valued by ;
g is ManySortedSet of n by ;
hence x in Bags n by ; :: thesis: verum
end;
assume x in Bags n ; :: thesis: x in the carrier of (product ())
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 ()) & ( for i being object st i in dom (Carrier ()) holds
g . i in (Carrier ()) . i ) )
take g = g; :: thesis: ( x = g & dom g = dom (Carrier ()) & ( for i being object st i in dom (Carrier ()) holds
g . i in (Carrier ()) . i ) )

thus x = g ; :: thesis: ( dom g = dom (Carrier ()) & ( for i being object st i in dom (Carrier ()) holds
g . i in (Carrier ()) . i ) )

thus dom g = dom (Carrier ()) by ; :: thesis: for i being object st i in dom (Carrier ()) holds
g . i in (Carrier ()) . i

let i be object ; :: thesis: ( i in dom (Carrier ()) implies g . i in (Carrier ()) . i )
assume i in dom (Carrier ()) ; :: thesis: g . i in (Carrier ()) . i
then A13: i in n ;
reconsider ii = i as set by TARSKI:1;
consider R being 1-sorted such that
A14: R = () . ii and
A15: (Carrier ()) . ii = the carrier of R by ;
R = OrderedNAT by
.= RelStr(# NAT,NATOrd #) by DICKSON:def 15 ;
then g . ii in (Carrier ()) . ii by A15;
hence g . i in (Carrier ()) . i ; :: thesis: verum
end;
then x in product (Carrier ()) by CARD_3:def 5;
hence x in the carrier of (product ()) by YELLOW_1:def 4; :: thesis: verum
end;
hence the carrier of (product ()) = Bags n by TARSKI:2; :: thesis: verum