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;

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)) ) )

hence
the carrier of (product (n --> OrderedNAT)) = Bags n
by TARSKI:2; :: thesis: verum( ( 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)) ) )

then reconsider g = x as natural-valued finite-support ManySortedSet of n ;

A12: dom g = n by PARTFUN1:def 2;

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

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

assume
x in Bags n
; :: thesis: 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

.= 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;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

A10: dom g =
dom (Carrier (n --> OrderedNAT))
by A3
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;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

.= 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

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 ) )

then
x in product (Carrier (n --> OrderedNAT))
by CARD_3:def 5;( 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;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

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