let n be Nat; :: thesis:
reconsider n0 = n as Element of NAT by ORDINAL1:def 12;
set CNOB = the carrier of ;
set IROB = the InternalRel of ;
set CP = the carrier of (product ());
set IP = the InternalRel of (product ());
the carrier of = Bags n by Def11;
then A1: the carrier of = the carrier of (product ()) by Th29;
now :: thesis: for a, b being object holds
( ( [a,b] in the InternalRel of implies [a,b] in the InternalRel of (product ()) ) & ( [a,b] in the InternalRel of (product ()) implies [a,b] in the InternalRel of ) )
let a, b be object ; :: thesis: ( ( [a,b] in the InternalRel of implies [a,b] in the InternalRel of (product ()) ) & ( [a,b] in the InternalRel of (product ()) implies [a,b] in the InternalRel of ) )
hereby :: thesis: ( [a,b] in the InternalRel of (product ()) implies [a,b] in the InternalRel of )
assume A2: [a,b] in the InternalRel of ; :: thesis: [a,b] in the InternalRel of (product ())
then A3: a in dom the InternalRel of by XTUPLE_0:def 12;
A4: b in rng the InternalRel of by ;
A5: a in the carrier of by A3;
A6: b in the carrier of by A4;
A7: a in Bags n by ;
A8: b in Bags n by ;
then reconsider a9 = a, b9 = b as Element of the carrier of (product ()) by ;
a9 in the carrier of (product ()) ;
then A9: a9 in product (Carrier ()) 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 = () . 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 = () . 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 = () . 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 = () . 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 = () . 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 = () . i & xi = f . i & yi = g . i & xi <= yi )

set R = () . i;
A13: (n --> OrderedNAT) . i = OrderedNAT by ;
reconsider R = () . i as RelStr by ;
take R = R; :: thesis: ex xi, yi being Element of R st
( R = () . i & xi = f . i & yi = g . i & xi <= yi )

set xi = f . i;
set yi = g . i;
dom f = n by ;
then A14: f . i in rng f by ;
A15: rng f c= NAT by ;
dom g = n by ;
then A16: g . i in rng g by ;
A17: rng g c= NAT by ;
then reconsider xi = f . i, yi = g . i as Element of R by ;
take xi = xi; :: thesis: ex yi being Element of R st
( R = () . i & xi = f . i & yi = g . i & xi <= yi )

take yi = yi; :: thesis: ( R = () . i & xi = f . i & yi = g . i & xi <= yi )
thus ( R = () . 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 ;
then a99 . i <= b99 . i by PRE_POLY:def 11;
then [xi,yi] in NATOrd by ;
hence xi <= yi by ; :: thesis: verum
end;
then a9 <= b9 by ;
hence [a,b] in the InternalRel of (product ()) by ORDERS_2:def 5; :: thesis: verum
end;
assume A19: [a,b] in the InternalRel of (product ()) ; :: thesis: [a,b] in the InternalRel of
then A20: a in dom the InternalRel of (product ()) by XTUPLE_0:def 12;
A21: b in rng the InternalRel of (product ()) by ;
A22: a in the carrier of (product ()) by A20;
A23: b in the carrier of (product ()) by A21;
A24: a in Bags n by ;
b in Bags n by ;
then reconsider a9 = a, b9 = b as bag of n by A24;
reconsider a2 = a9, b2 = b9 as Element of the carrier of (product ()) by ;
a2 in the carrier of (product ()) ;
then A25: a2 in product (Carrier ()) by YELLOW_1:def 4;
a2 <= b2 by ;
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 = () . i & xi = f . i & yi = g . i & xi <= yi ) by ;
now :: thesis: for k being object st k in n holds
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 = () . k and
A31: xi = f . k and
A32: yi = g . k and
A33: xi <= yi by ;
R = OrderedNAT by ;
then [xi,yi] in NATOrd by ;
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 ;
hence a9 . k <= b9 . k by ; :: thesis: verum
end;
then a9 divides b9 by PRE_POLY:46;
hence [a,b] in the InternalRel of by Def11; :: thesis: verum
end;
hence NaivelyOrderedBags n = product () by ; :: thesis: verum