set R = RelStr(# (Bags n),(DivOrder n) #);
set S = product (Carrier (n --> OrderedNAT ));
set SJ = Carrier (n --> OrderedNAT );
set P = product (n --> OrderedNAT );
set J = n --> OrderedNAT ;
defpred S₁[ set , set ] means ( n in product (Carrier (n --> OrderedNAT )) & ex b being bag of st
( b = c₂ & b = n ) );
A1: for x being set st x in product (Carrier (n --> OrderedNAT )) holds
for g being Function st x = g holds
( dom g = n & ( for y being set st y in dom g holds
g . y in NAT ) )

proof

let x be set ; :: thesis:
assume x in product (Carrier (n --> OrderedNAT )) ; :: thesis:
then consider g being Function such that
A2: x = g and
A3: dom g = dom (Carrier (n --> OrderedNAT )) and
A4: for y being set st y in dom (Carrier (n --> OrderedNAT )) holds
g . y in (Carrier (n --> OrderedNAT )) . y by CARD_3:def 5;
let g' be Function; :: thesis:
assume A5: x = g' ; :: thesis:
hence dom g' = n by A2, A3, PARTFUN1:def 4; :: thesis:
thus for y being set st y in dom g' holds
g' . y in NAT :: thesis:

proof

let y be set ; :: thesis:
assume A6: y in dom g' ; :: thesis:
then A7: y in n by A5, A2, A3, PARTFUN1:def 4;
then consider R being 1-sorted such that
A8: R = (n --> OrderedNAT ) . y and
A9: (Carrier (n --> OrderedNAT )) . y = the carrier of R by PRALG_1:def 13;
g . y in the carrier of R by A5, A2, A3, A4, A6, A9;
hence g' . y in NAT by A5, A2, A7, A8, DICKSON:def 15, FUNCOP_1:13; :: thesis:

end;

A10: for x being set st x in product (Carrier (n --> OrderedNAT )) holds
ex y being set st S₁[x,y]

proof

let x be set ; :: thesis:
assume A11: x in product (Carrier (n --> OrderedNAT )) ; :: thesis:
then consider g being Function such that
A12: x = g and
dom g = dom (Carrier (n --> OrderedNAT )) and
for y being set st y in dom (Carrier (n --> OrderedNAT )) holds
g . y in (Carrier (n --> OrderedNAT )) . y by CARD_3:def 5;
defpred S₂[ set , set ] means c₂ = g . n;
A13: for x being set st x in n holds
ex y being set st S₂[x,y] ;
consider b being Function such that
A14: ( dom b = n & ( for x being set st x in n holds
S₂[x,b . x] ) ) from CLASSES1:sch 1(A13);
reconsider b = b as ManySortedSet of by A14, PARTFUN1:def 4, RELAT_1:def 18;
A15: dom g = n by A1, A11, A12;

now

let u be set ; :: thesis:
assume u in rng b ; :: thesis:
then consider x being set such that
A16: ( x in dom b & u = b . x ) by FUNCT_1:def 5;
( u = g . x & x in dom g ) by A15, A14, A16, PARTFUN1:def 4;
hence u in NAT by A1, A11, A12; :: thesis:

end;

then rng b c= NAT by TARSKI:def 3;
then reconsider b = b as bag of by VALUED_0:def 6;
take b ; :: thesis:
thus x in product (Carrier (n --> OrderedNAT )) by A11; :: thesis:
take b ; :: thesis:
thus b = b ; :: thesis:
thus b = x by A12, A15, A14, FUNCT_1:9; :: thesis:

end;

consider i being Function such that
A17: ( dom i = product (Carrier (n --> OrderedNAT )) & ( for x being set st x in product (Carrier (n --> OrderedNAT )) holds
S₁[x,i . x] ) ) from CLASSES1:sch 1(A10);
A18: for x being Element of RelStr(# (Bags n),(DivOrder n) #) ex u being Element of (product (n --> OrderedNAT )) st
( u in dom i & i . u = x )

proof

let x be Element of RelStr(# (Bags n),(DivOrder n) #); :: thesis:
reconsider g = x as bag of by PRE_POLY:def 12;

A19: now

let x be set ; :: thesis:
assume x in dom (Carrier (n --> OrderedNAT )) ; :: thesis:
then A20: x in n by PARTFUN1:def 4;
then consider L being 1-sorted such that
A21: L = (n --> OrderedNAT ) . x and
A22: (Carrier (n --> OrderedNAT )) . x = the carrier of L by PRALG_1:def 13;
the carrier of L = NAT by A20, A21, DICKSON:def 15, FUNCOP_1:13;
hence g . x in (Carrier (n --> OrderedNAT )) . x by A22; :: thesis:

end;

A23: dom g = n by PARTFUN1:def 4
.= dom (Carrier (n --> OrderedNAT )) by PARTFUN1:def 4 ;
then A24: g in product (Carrier (n --> OrderedNAT )) by A19, CARD_3:def 5;
then reconsider g = g as Element of (product (n --> OrderedNAT )) by YELLOW_1:def 4;
take g ; :: thesis:
thus g in dom i by A17, A23, A19, CARD_3:def 5; :: thesis:
S₁[g,i . g] by A17, A24;
hence i . g = x ; :: thesis:

end;

A25: now

let v be set ; :: thesis:
assume v in rng i ; :: thesis:
then consider u being set such that
A26: u in dom i and
A27: v = i . u by FUNCT_1:def 5;
ex b being bag of st
( b = i . u & b = u ) by A17, A26;
hence v in Bags n by A27, PRE_POLY:def 12; :: thesis:

end;

now

let N be Subset of RelStr(# (Bags n),(DivOrder n) #); :: thesis:
set N' = i " N;
A28: i " N c= product (Carrier (n --> OrderedNAT )) by A17, RELAT_1:167;
then reconsider N' = i " N as Subset of (product (n --> OrderedNAT )) by YELLOW_1:def 4;
consider B' being set such that
A29: B' is_Dickson-basis_of N', product (n --> OrderedNAT ) and
A30: B' is finite by DICKSON:def 10;
set B = i .: B';
A31: B' c= N' by A29, DICKSON:def 9;
A32: for a, b being Element of (product (n --> OrderedNAT ))
for ta, tb being Element of Bags n st a = ta & b = tb & a in product (Carrier (n --> OrderedNAT )) & a <= b holds
ta divides tb

proof

let a, b be Element of (product (n --> OrderedNAT )); :: thesis:
let ta, tb be Element of Bags n; :: thesis:
assume that
A33: ( a = ta & b = tb ) and
A34: a in product (Carrier (n --> OrderedNAT )) ; :: thesis:
assume a <= b ; :: thesis:
then consider f, g being Function such that
A35: ( f = a & g = b ) and
A36: for i being set st i in n holds
ex R being RelStr ex ai, bi being Element of R st
( R = (n --> OrderedNAT ) . i & ai = f . i & bi = g . i & ai <= bi ) by A34, YELLOW_1:def 4;

now

let k be set ; :: thesis:
assume A37: k in n ; :: thesis:
then consider R being RelStr , ak, bk being Element of R such that
A38: R = (n --> OrderedNAT ) . k and
A39: ( ak = f . k & bk = g . k ) and
A40: ak <= bk by A36;
(n --> OrderedNAT ) . k = OrderedNAT by A37, FUNCOP_1:13;
then [ak,bk] in NATOrd by A38, A40, DICKSON:def 15, ORDERS_2:def 9;
then consider a', b' being Element of NAT such that
A41: [a',b'] = [ak,bk] and
A42: a' <= b' by DICKSON:def 14;
A43: b' = [ak,bk] `2 by A41, MCART_1:def 2
.= bk by MCART_1:def 2 ;
a' = [ak,bk] `1 by A41, MCART_1:def 1
.= ak by MCART_1:def 1 ;
hence ta . k <= tb . k by A33, A35, A39, A42, A43; :: thesis:

end;

hence ta divides tb by PRE_POLY:46; :: thesis:

end;

A44: for a being Element of RelStr(# (Bags n),(DivOrder n) #) st a in N holds
ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in i .: B' & b <= a )

proof

let a be Element of RelStr(# (Bags n),(DivOrder n) #); :: thesis:
consider a' being Element of (product (n --> OrderedNAT )) such that
A45: a' in dom i and
A46: i . a' = a by A18;
A47: ex b being bag of st
( b = i . a' & b = a' ) by A17, A45;
assume a in N ; :: thesis:
then a' in N' by A45, A46, FUNCT_1:def 13;
then consider b' being Element of (product (n --> OrderedNAT )) such that
A48: b' in B' and
A49: b' <= a' by A29, DICKSON:def 9;
set b = i . b';
A50: B' c= product (Carrier (n --> OrderedNAT )) by A28, A31, XBOOLE_1:1;
then i . b' in rng i by A17, A48, FUNCT_1:def 5;
then reconsider b = i . b' as Element of Bags n by A25;
reconsider b = b as Element of RelStr(# (Bags n),(DivOrder n) #) ;
take b ; :: thesis:
thus b in i .: B' by A17, A48, A50, FUNCT_1:def 12; :: thesis:
reconsider aa = a, bb = b as Element of Bags n ;
ex b1 being bag of st
( b1 = i . b' & b1 = b' ) by A17, A48, A50;
then bb divides aa by A32, A46, A47, A48, A49, A50;
then [b,a] in DivOrder n by Def5;
hence b <= a by ORDERS_2:def 9; :: thesis:

end;

now

let u be set ; :: thesis:
assume u in i .: B' ; :: thesis:
then ex v being set st
( v in dom i & v in B' & u = i . v ) by FUNCT_1:def 12;
hence u in N by A31, FUNCT_1:def 13; :: thesis:

end;

then i .: B' c= N by TARSKI:def 3;
then i .: B' is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #) by A44, DICKSON:def 9;
hence ex B being set st
( B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #) & B is finite ) by A30; :: thesis:

end;

hence RelStr(# (Bags n),(DivOrder n) #) is Dickson by DICKSON:def 10; :: thesis: