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 Def13;
then A1:
the carrier of (NaivelyOrderedBags n) = the carrier of (product (n --> OrderedNAT))
by Th33;
now let a,
b be
set ;
( ( [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 RELAT_1:6;
A4:
b in rng the
InternalRel of
(NaivelyOrderedBags n)
by A2, RELAT_1:6;
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, Def13;
A8:
b in Bags n
by A6, Def13;
then reconsider a9 =
a,
b9 =
b as
Element of the
carrier of
(product (n --> OrderedNAT)) by A7, Th33;
a9 in the
carrier of
(product (n0 --> OrderedNAT))
;
then A9:
a9 in product (Carrier (n --> OrderedNAT))
by YELLOW_1:def 4;
now 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 set 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 set 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 set 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
set ;
( 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;
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;
a99 divides b99
by A2, Def13;
then
a99 . i <= b99 . i
by PRE_POLY:def 11;
then
[xi,yi] in NATOrd
by DICKSON:def 14;
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 A17:
[a,b] in the
InternalRel of
(product (n --> OrderedNAT))
;
[a,b] in the InternalRel of (NaivelyOrderedBags n)then A18:
a in dom the
InternalRel of
(product (n --> OrderedNAT))
by RELAT_1:6;
A19:
b in rng the
InternalRel of
(product (n --> OrderedNAT))
by A17, RELAT_1:6;
A20:
a in the
carrier of
(product (n --> OrderedNAT))
by A18;
A21:
b in the
carrier of
(product (n --> OrderedNAT))
by A19;
A22:
a in Bags n
by A20, Th33;
b in Bags n
by A21, Th33;
then reconsider a9 =
a,
b9 =
b as
bag of
n by A22;
reconsider a2 =
a9,
b2 =
b9 as
Element of the
carrier of
(product (n --> OrderedNAT)) by A18, A19;
a2 in the
carrier of
(product (n0 --> OrderedNAT))
;
then A23:
a2 in product (Carrier (n --> OrderedNAT))
by YELLOW_1:def 4;
a2 <= b2
by A17, ORDERS_2:def 5;
then consider f,
g being
Function such that A24:
f = a2
and A25:
g = b2
and A26:
for
i being
set 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 A23, YELLOW_1:def 4;
now let k be
set ;
( k in n implies a9 . k <= b9 . k )assume A27:
k in n
;
a9 . k <= b9 . kconsider R being
RelStr ,
xi,
yi being
Element of
R such that A28:
R = (n --> OrderedNAT) . k
and A29:
xi = f . k
and A30:
yi = g . k
and A31:
xi <= yi
by A26, A27;
R = OrderedNAT
by A27, A28, FUNCOP_1:7;
then
[xi,yi] in NATOrd
by A31, DICKSON:def 15, ORDERS_2:def 5;
then consider xii,
yii being
Element of
NAT such that A32:
[xii,yii] = [xi,yi]
and A33:
xii <= yii
by DICKSON:def 14;
xii = xi
by A32, ZFMISC_1:27;
hence
a9 . k <= b9 . k
by A24, A25, A29, A30, A32, A33, ZFMISC_1:27;
verum end; then
a9 divides b9
by PRE_POLY:46;
hence
[a,b] in the
InternalRel of
(NaivelyOrderedBags n)
by Def13;
verum end;
hence
NaivelyOrderedBags n = product (n --> OrderedNAT)
by A1, RELAT_1:def 2; verum