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;

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

hence
NaivelyOrderedBags n = product (n --> OrderedNAT)
by A1, RELAT_1:def 2; :: thesis: verum( ( [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) ) )

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;

hence [a,b] in the InternalRel of (NaivelyOrderedBags n) by Def11; :: thesis: verum

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

assume A19:
[a,b] in the InternalRel of (product (n --> OrderedNAT))
; :: thesis: [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;

hence [a,b] in the InternalRel of (product (n --> OrderedNAT)) by ORDERS_2:def 5; :: thesis: verum

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

then
a9 <= b9
by A9, YELLOW_1:def 4;( 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;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

hence [a,b] in the InternalRel of (product (n --> OrderedNAT)) by ORDERS_2:def 5; :: thesis: verum

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

then
a9 divides b9
by PRE_POLY:46;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;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

hence [a,b] in the InternalRel of (NaivelyOrderedBags n) by Def11; :: thesis: verum