let n be Nat; NaivelyOrderedBags n = product (n --> OrderedNAT )
reconsider n0 = n as Element of NAT by ORDINAL1:def 13;
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:20;
A4:
b in rng the
InternalRel of
(NaivelyOrderedBags n)
by A2, RELAT_1:20;
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 a' =
a,
b' =
b as
Element of the
carrier of
(product (n --> OrderedNAT )) by A7, Th33;
a' in the
carrier of
(product (n0 --> OrderedNAT ))
;
then A9:
a' in product (Carrier (n --> OrderedNAT ))
by YELLOW_1:def 4;
now set f =
a';
set g =
b';
A10:
a' is
bag of
n
by A7, PRE_POLY:def 12;
A11:
b is
bag of
n
by A8, PRE_POLY:def 12;
reconsider f =
a',
g =
b' as
Function by A7, A8, PRE_POLY:def 12;
take f =
f;
ex g being Function st
( f = a' & g = b' & ( for i being set st i in n holds
ex R being RelStr ex xi, yi being Element of st
( R = (n --> OrderedNAT ) . i & xi = f . i & yi = g . i & xi <= yi ) ) )take g =
g;
( f = a' & g = b' & ( for i being set st i in n holds
ex R being RelStr ex xi, yi being Element of st
( R = (n --> OrderedNAT ) . i & xi = f . i & yi = g . i & xi <= yi ) ) )thus
(
f = a' &
g = b' )
;
for i being set st i in n holds
ex R being RelStr ex xi, yi being Element of 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 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 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:13;
reconsider R =
(n --> OrderedNAT ) . i as
RelStr by A12, FUNCOP_1:13;
take R =
R;
ex xi, yi being Element of 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 4;
then A14:
f . i in rng f
by A12, FUNCT_1:12;
A15:
rng f c= NAT
by A10, VALUED_0:def 6;
dom g = n
by A11, PARTFUN1:def 4;
then A16:
g . i in rng g
by A12, FUNCT_1:12;
rng g c= NAT
by A11, VALUED_0:def 6;
then reconsider xi =
f . i,
yi =
g . i as
Element of
by A12, A14, A15, A16, DICKSON:def 15, FUNCOP_1:13;
take xi =
xi;
ex yi being Element of 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 a'' =
a',
b'' =
b' as
bag of
n by A7, A8, PRE_POLY:def 12;
a'' divides b''
by A2, Def13;
then
a'' . i <= b'' . 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 9;
verum end; then
a' <= b'
by A9, YELLOW_1:def 4;
hence
[a,b] in the
InternalRel of
(product (n --> OrderedNAT ))
by ORDERS_2:def 9;
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:20;
A19:
b in rng the
InternalRel of
(product (n --> OrderedNAT ))
by A17, RELAT_1:20;
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 a' =
a,
b' =
b as
bag of
n by A22, PRE_POLY:def 12;
reconsider a2 =
a',
b2 =
b' 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 9;
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 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 a' . k <= b' . k )assume A27:
k in n
;
a' . k <= b' . kconsider R being
RelStr ,
xi,
yi being
Element of
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:13;
then
[xi,yi] in NATOrd
by A31, DICKSON:def 15, ORDERS_2:def 9;
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:33;
hence
a' . k <= b' . k
by A24, A25, A29, A30, A32, A33, ZFMISC_1:33;
verum end; then
a' divides b'
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