let n be Nat; 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 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 ;
( ( [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 ( [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)
;
[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 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;
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;
( 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 )
;
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 ;
( 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
;
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;
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;
ex yi being Element of R st
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi )take yi =
yi;
( R = (n --> OrderedNAT) . i & xi = f . i & yi = g . i & xi <= yi )thus
(
R = (n --> OrderedNAT) . i &
xi = f . i &
yi = g . i )
;
xi <= yireconsider 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;
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;
verum
end; assume A19:
[a,b] in the
InternalRel of
(product (n --> OrderedNAT))
;
[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 for k being object st k in n holds
a9 . k <= b9 . klet k be
object ;
( k in n implies a9 . k <= b9 . k )assume A29:
k in n
;
a9 . k <= b9 . kconsider 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;
verum end; then
a9 divides b9
by PRE_POLY:46;
hence
[a,b] in the
InternalRel of
(NaivelyOrderedBags n)
by Def11;
verum end;
hence
NaivelyOrderedBags n = product (n --> OrderedNAT)
by A1, RELAT_1:def 2; verum