let n be Nat; :: thesis: NaivelyOrderedBags n = product (n --> OrderedNAT)
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
set CNOB = the carrier of (NaivelyOrderedBags n);
set IROB = the InternalRel of (NaivelyOrderedBags n);
set CP = the carrier of (product (n --> OrderedNAT));
set IP = the InternalRel of (product (n --> OrderedNAT));
the carrier of (NaivelyOrderedBags n) = Bags n by Def11;
then A1: the carrier of (NaivelyOrderedBags n) = the carrier of (product (n --> OrderedNAT)) by Th29;

now :: thesis: for a, b being object holds
( ( [a,b] in the InternalRel of (NaivelyOrderedBags n) implies [a,b] in the InternalRel of (product (n --> OrderedNAT)) ) & ( [a,b] in the InternalRel of (product (n --> OrderedNAT)) implies [a,b] in the InternalRel of (NaivelyOrderedBags n) ) )

let a, b be object ; :: thesis: ( ( [a,b] in the InternalRel of (NaivelyOrderedBags n) implies [a,b] in the InternalRel of (product (n --> OrderedNAT)) ) & ( [a,b] in the InternalRel of (product (n --> OrderedNAT)) implies [a,b] in the InternalRel of (NaivelyOrderedBags n) ) )

hereby :: thesis: ( [a,b] in the InternalRel of (product (n --> OrderedNAT)) implies [a,b] in the InternalRel of (NaivelyOrderedBags n) )

assume A2: [a,b] in the InternalRel of (NaivelyOrderedBags n) ; :: thesis: [a,b] in the InternalRel of (product (n --> OrderedNAT))
then A3: a in dom the InternalRel of (NaivelyOrderedBags n) by XTUPLE_0:def 12;
A4: b in rng the InternalRel of (NaivelyOrderedBags n) by A2, XTUPLE_0:def 13;
A5: a in the carrier of (NaivelyOrderedBags n) by A3;
A6: b in the carrier of (NaivelyOrderedBags n) by A4;
A7: a in Bags n by A5, Def11;
A8: b in Bags n by A6, Def11;
then reconsider a9 = a, b9 = b as Element of the carrier of (product (n --> OrderedNAT)) by A7, Th29;
a9 in the carrier of (product (n0 --> OrderedNAT)) ;
then A9: a9 in product (Carrier (n --> OrderedNAT)) by YELLOW_1:def 4;

now :: thesis: ex f, g being Function st
( f = a9 & g = b9 & ( for i being object st i in n holds
ex R being RelStr ex xi, yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi ) ) )

set f = a9;
set g = b9;
A10: a9 is bag of n by A7;
A11: b is bag of n by A8;
reconsider f = a9, g = b9 as Function by A7, A8;
take f = f; :: thesis: ex g being Function st
( f = a9 & g = b9 & ( for i being object st i in n holds
ex R being RelStr ex xi, yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
take g = g; :: thesis: ( f = a9 & g = b9 & ( for i being object st i in n holds
ex R being RelStr ex xi, yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi ) ) )
thus ( f = a9 & g = b9 ) ; :: thesis: for i being object st i in n holds
ex R being RelStr ex xi, yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi )
let i be object ; :: thesis: ( i in n implies ex R being RelStr ex xi, yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi ) )
assume A12: i in n ; :: thesis: ex R being RelStr ex xi, yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi )
set R = (n --> OrderedNAT) . i;
A13: (n --> OrderedNAT) . i = OrderedNAT by A12, FUNCOP_1:7;
reconsider R = (n --> OrderedNAT) . i as RelStr by A12, FUNCOP_1:7;
take R = R; :: thesis: ex xi, yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi )
set xi = f . i;
set yi = g . i;
dom f = n by A10, PARTFUN1:def 2;
then A14: f . i in rng f by A12, FUNCT_1:3;
A15: rng f c= NAT by A10, VALUED_0:def 6;
dom g = n by A11, PARTFUN1:def 2;
then A16: g . i in rng g by A12, FUNCT_1:3;
A17: rng g c= NAT by A11, VALUED_0:def 6;
then reconsider xi = f . i, yi = g . i as Element of R by A12, A14, A15, A16, DICKSON:def 15, FUNCOP_1:7;
take xi = xi; :: thesis: ex yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi )
take yi = yi; :: thesis: ( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi )
thus ( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i ) ; :: thesis: xi <= yi
reconsider a99 = a9, b99 = b9 as bag of n by A7, A8;
A18: ( xi in NAT & yi in NAT ) by A15, A17, A14, A16;
a99 divides b99 by A2, Def11;
then a99 . i <= b99 . i by PRE_POLY:def 11;
then [xi,yi] in NATOrd by DICKSON:def 14, A18;
hence xi <= yi by A13, DICKSON:def 15, ORDERS_2:def 5; :: thesis: verum

end;

then a9 <= b9 by A9, YELLOW_1:def 4;
hence [a,b] in the InternalRel of (product (n --> OrderedNAT)) by ORDERS_2:def 5; :: thesis: verum

end;

assume A19: [a,b] in the InternalRel of (product (n --> OrderedNAT)) ; :: thesis: [a,b] in the InternalRel of (NaivelyOrderedBags n)
then A20: a in dom the InternalRel of (product (n --> OrderedNAT)) by XTUPLE_0:def 12;
A21: b in rng the InternalRel of (product (n --> OrderedNAT)) by A19, XTUPLE_0:def 13;
A22: a in the carrier of (product (n --> OrderedNAT)) by A20;
A23: b in the carrier of (product (n --> OrderedNAT)) by A21;
A24: a in Bags n by A22, Th29;
b in Bags n by A23, Th29;
then reconsider a9 = a, b9 = b as bag of n by A24;
reconsider a2 = a9, b2 = b9 as Element of the carrier of (product (n --> OrderedNAT)) by A20, A21;
a2 in the carrier of (product (n0 --> OrderedNAT)) ;
then A25: a2 in product (Carrier (n --> OrderedNAT)) by YELLOW_1:def 4;
a2 <= b2 by A19, ORDERS_2:def 5;
then consider f, g being Function such that
A26: f = a2 and
A27: g = b2 and
A28: for i being object st i in n holds
ex R being RelStr ex xi, yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi ) by A25, YELLOW_1:def 4;

now :: thesis: for k being object st k in n holds
a9 . k <= b9 . k

let k be object ; :: thesis: ( k in n implies a9 . k <= b9 . k )
assume A29: k in n ; :: thesis: a9 . k <= b9 . k
consider R being RelStr , xi, yi being Element of R such that
A30: R = (n --> OrderedNAT) . k and
A31: xi = f . k and
A32: yi = g . k and
A33: xi <= yi by A28, A29;
R = OrderedNAT by A29, A30, FUNCOP_1:7;
then [xi,yi] in NATOrd by A33, DICKSON:def 15, ORDERS_2:def 5;
then consider xii, yii being Element of NAT such that
A34: [xii,yii] = [xi,yi] and
A35: xii <= yii by DICKSON:def 14;
xii = xi by A34, XTUPLE_0:1;
hence a9 . k <= b9 . k by A26, A27, A31, A32, A34, A35, XTUPLE_0:1; :: thesis: verum

end;

then a9 divides b9 by PRE_POLY:46;
hence [a,b] in the InternalRel of (NaivelyOrderedBags n) by Def11; :: thesis: verum

end;

hence NaivelyOrderedBags n = product (n --> OrderedNAT) by A1, RELAT_1:def 2; :: thesis: verum