let n be Element of NAT ; :: thesis: NaivelyOrderedBags n = product (n --> OrderedNAT )
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 ;
:: 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
(
a in dom the
InternalRel of
(NaivelyOrderedBags n) &
b in rng the
InternalRel of
(NaivelyOrderedBags n) )
by RELAT_1:20;
then
(
a in the
carrier of
(NaivelyOrderedBags n) &
b in the
carrier of
(NaivelyOrderedBags n) )
;
then A3:
(
a in Bags n &
b in Bags n )
by Def13;
then reconsider a' =
a,
b' =
b as
Element of the
carrier of
(product (n --> OrderedNAT )) by Th33;
a' in the
carrier of
(product (n --> OrderedNAT ))
;
then A4:
a' in product (Carrier (n --> OrderedNAT ))
by YELLOW_1:def 4;
now set f =
a';
set g =
b';
A5:
(
a' is
bag of &
b is
bag of )
by A3, POLYNOM1:def 14;
reconsider f =
a',
g =
b' as
Function by A3, POLYNOM1:def 14;
take f =
f;
:: thesis: 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 R st
( R = (n --> OrderedNAT ) . i & xi = f . i & yi = g . i & xi <= yi ) ) )take g =
g;
:: thesis: ( f = a' & g = b' & ( 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 = a' &
g = b' )
;
:: thesis: 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 ;
:: 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 A6:
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;
A7:
(n --> OrderedNAT ) . i = OrderedNAT
by A6, FUNCOP_1:13;
reconsider R =
(n --> OrderedNAT ) . i as
RelStr by A6, FUNCOP_1:13;
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 A5, PARTFUN1:def 4;
then A8:
f . i in rng f
by A6, FUNCT_1:12;
A9:
rng f c= NAT
by A5, VALUED_0:def 6;
dom g = n
by A5, PARTFUN1:def 4;
then A10:
g . i in rng g
by A6, FUNCT_1:12;
rng g c= NAT
by A5, VALUED_0:def 6;
then reconsider xi =
f . i,
yi =
g . i as
Element of
R by A6, A8, A9, A10, DICKSON:def 15, FUNCOP_1:13;
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 <= yireconsider a'' =
a',
b'' =
b' as
bag of
by A3, POLYNOM1:def 14;
a'' divides b''
by A2, Def13;
then
a'' . i <= b'' . i
by POLYNOM1:def 13;
then
[xi,yi] in NATOrd
by DICKSON:def 14;
hence
xi <= yi
by A7, DICKSON:def 15, ORDERS_2:def 9;
:: thesis: verum end; then
a' <= b'
by A4, YELLOW_1:def 4;
hence
[a,b] in the
InternalRel of
(product (n --> OrderedNAT ))
by ORDERS_2:def 9;
:: thesis: verum
end; assume A11:
[a,b] in the
InternalRel of
(product (n --> OrderedNAT ))
;
:: thesis: [a,b] in the InternalRel of (NaivelyOrderedBags n)then A12:
(
a in dom the
InternalRel of
(product (n --> OrderedNAT )) &
b in rng the
InternalRel of
(product (n --> OrderedNAT )) )
by RELAT_1:20;
then
(
a in the
carrier of
(product (n --> OrderedNAT )) &
b in the
carrier of
(product (n --> OrderedNAT )) )
;
then
(
a in Bags n &
b in Bags n )
by Th33;
then reconsider a' =
a,
b' =
b as
bag of
by POLYNOM1:def 14;
reconsider a2 =
a',
b2 =
b' as
Element of the
carrier of
(product (n --> OrderedNAT )) by A12;
a2 in the
carrier of
(product (n --> OrderedNAT ))
;
then A13:
a2 in product (Carrier (n --> OrderedNAT ))
by YELLOW_1:def 4;
a2 <= b2
by A11, ORDERS_2:def 9;
then consider f,
g being
Function such that A14:
(
f = a2 &
g = b2 )
and A15:
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 A13, YELLOW_1:def 4;
now let k be
set ;
:: thesis: ( k in n implies a' . k <= b' . k )assume A16:
k in n
;
:: thesis: a' . k <= b' . kconsider R being
RelStr ,
xi,
yi being
Element of
R such that A17:
R = (n --> OrderedNAT ) . k
and A18:
(
xi = f . k &
yi = g . k )
and A19:
xi <= yi
by A15, A16;
R = OrderedNAT
by A16, A17, FUNCOP_1:13;
then
[xi,yi] in NATOrd
by A19, DICKSON:def 15, ORDERS_2:def 9;
then consider xii,
yii being
Element of
NAT such that A20:
[xii,yii] = [xi,yi]
and A21:
xii <= yii
by DICKSON:def 14;
(
xii = xi &
yii = yi )
by A20, ZFMISC_1:33;
hence
a' . k <= b' . k
by A14, A18, A21;
:: thesis: verum end; then
a' divides b'
by POLYNOM1:50;
hence
[a,b] in the
InternalRel of
(NaivelyOrderedBags n)
by Def13;
:: thesis: verum end;
hence
NaivelyOrderedBags n = product (n --> OrderedNAT )
by A1, RELAT_1:def 2; :: thesis: verum