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₁[ object , object ] means ( n in product (Carrier (n --> OrderedNAT)) & ex b being bag of n 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: ( x in product (Carrier (n --> OrderedNAT)) implies 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 ) ) )
assume x in product (Carrier (n --> OrderedNAT)) ; :: thesis: 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 ) )
then consider g being Function such that
A2: x = g and
A3: dom g = dom (Carrier (n --> OrderedNAT)) and
A4: for y being object st y in dom (Carrier (n --> OrderedNAT)) holds
g . y in (Carrier (n --> OrderedNAT)) . y by CARD_3:def 5;
let g9 be Function; :: thesis: ( x = g9 implies ( dom g9 = n & ( for y being set st y in dom g9 holds
g9 . y in NAT ) ) )
assume A5: x = g9 ; :: thesis: ( dom g9 = n & ( for y being set st y in dom g9 holds
g9 . y in NAT ) )
hence dom g9 = n by A2, A3, PARTFUN1:def 2; :: thesis: for y being set st y in dom g9 holds
g9 . y in NAT
thus for y being set st y in dom g9 holds
g9 . y in NAT :: thesis: verum

proof

let y be set ; :: thesis: ( y in dom g9 implies g9 . y in NAT )
assume A6: y in dom g9 ; :: thesis: g9 . y in NAT
then A7: y in n by A5, A2, A3;
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 15;
g . y in the carrier of R by A5, A2, A3, A4, A6, A9;
hence g9 . y in NAT by A5, A2, A7, A8, DICKSON:def 15, FUNCOP_1:7; :: thesis: verum

end;

end;

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

proof

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

now :: thesis: for u being object st u in rng b holds
u in NAT

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

end;

then rng b c= NAT ;
then reconsider b = b as bag of n by VALUED_0:def 6;
take b ; :: thesis: S₁[x,b]
thus x in product (Carrier (n --> OrderedNAT)) by A11; :: thesis: ex b being bag of n st
( b = b & b = x )
take b ; :: thesis: ( b = b & b = x )
thus b = b ; :: thesis: b = x
b = g by A15, A14, FUNCT_1:2;
hence b = x by A12; :: thesis: verum

end;

consider i being Function such that
A17: ( dom i = product (Carrier (n --> OrderedNAT)) & ( for x being object 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: ex u being Element of (product (n --> OrderedNAT)) st
( u in dom i & i . u = x )
reconsider g = x as bag of n ;

A19: now :: thesis: for x being object st x in dom (Carrier (n --> OrderedNAT)) holds
g . x in (Carrier (n --> OrderedNAT)) . x

let x be object ; :: thesis: ( x in dom (Carrier (n --> OrderedNAT)) implies g . x in (Carrier (n --> OrderedNAT)) . x )
assume x in dom (Carrier (n --> OrderedNAT)) ; :: thesis: g . x in (Carrier (n --> OrderedNAT)) . x
then A20: x in n ;
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 15;
the carrier of L = NAT by A20, A21, DICKSON:def 15, FUNCOP_1:7;
hence g . x in (Carrier (n --> OrderedNAT)) . x by A22, ORDINAL1:def 12; :: thesis: verum

end;

A23: dom g = n by PARTFUN1:def 2
.= dom (Carrier (n --> OrderedNAT)) by PARTFUN1:def 2 ;
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: ( g in dom i & i . g = x )
thus g in dom i by A17, A23, A19, CARD_3:def 5; :: thesis: i . g = x
S₁[g,i . g] by A17, A24;
hence i . g = x ; :: thesis: verum

end;

A25: now :: thesis: for v being set st v in rng i holds
v in Bags n

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

end;

now :: thesis: for N being Subset of RelStr(# (Bags n),(DivOrder n) #) ex B being set st
( B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #) & B is finite )

let N be Subset of RelStr(# (Bags n),(DivOrder n) #); :: thesis: ex B being set st
( B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #) & B is finite )
set N9 = i " N;
A28: i " N c= product (Carrier (n --> OrderedNAT)) by A17, RELAT_1:132;
then reconsider N9 = i " N as Subset of (product (n --> OrderedNAT)) by YELLOW_1:def 4;
consider B9 being set such that
A29: B9 is_Dickson-basis_of N9, product (n --> OrderedNAT) and
A30: B9 is finite by DICKSON:def 10;
set B = i .: B9;
A31: B9 c= N9 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: 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
let ta, tb be Element of Bags n; :: thesis: ( a = ta & b = tb & a in product (Carrier (n --> OrderedNAT)) & a <= b implies ta divides tb )
assume that
A33: ( a = ta & b = tb ) and
A34: a in product (Carrier (n --> OrderedNAT)) ; :: thesis: ( not a <= b or ta divides tb )
assume a <= b ; :: thesis: ta divides tb
then consider f, g being Function such that
A35: ( f = a & g = b ) and
A36: for i being object 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 :: thesis: for k being object st k in n holds
ta . k <= tb . k

let k be object ; :: thesis: ( k in n implies ta . k <= tb . k )
assume A37: k in n ; :: thesis: ta . k <= tb . k
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:7;
then [ak,bk] in NATOrd by A38, A40, DICKSON:def 15, ORDERS_2:def 5;
then consider a9, b9 being Element of NAT such that
A41: [a9,b9] = [ak,bk] and
A42: a9 <= b9 by DICKSON:def 14;
A43: b9 = bk by A41, XTUPLE_0:1;
a9 = ak by A41, XTUPLE_0:1;
hence ta . k <= tb . k by A33, A35, A39, A42, A43; :: thesis: verum

end;

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

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 .: B9 & b <= a )

proof

let a be Element of RelStr(# (Bags n),(DivOrder n) #); :: thesis: ( a in N implies ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in i .: B9 & b <= a ) )
consider a9 being Element of (product (n --> OrderedNAT)) such that
A45: a9 in dom i and
A46: i . a9 = a by A18;
A47: ex b being bag of n st
( b = i . a9 & b = a9 ) by A17, A45;
assume a in N ; :: thesis: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in i .: B9 & b <= a )
then a9 in N9 by A45, A46, FUNCT_1:def 7;
then consider b9 being Element of (product (n --> OrderedNAT)) such that
A48: b9 in B9 and
A49: b9 <= a9 by A29, DICKSON:def 9;
set b = i . b9;
A50: B9 c= product (Carrier (n --> OrderedNAT)) by A28, A31;
then i . b9 in rng i by A17, A48, FUNCT_1:def 3;
then reconsider b = i . b9 as Element of Bags n by A25;
reconsider b = b as Element of RelStr(# (Bags n),(DivOrder n) #) ;
take b ; :: thesis: ( b in i .: B9 & b <= a )
thus b in i .: B9 by A17, A48, A50, FUNCT_1:def 6; :: thesis: b <= a
reconsider aa = a, bb = b as Element of Bags n ;
ex b1 being bag of n st
( b1 = i . b9 & b1 = b9 ) 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 5; :: thesis: verum

end;

now :: thesis: for u being object st u in i .: B9 holds
u in N

let u be object ; :: thesis: ( u in i .: B9 implies u in N )
assume u in i .: B9 ; :: thesis: u in N
then ex v being object st
( v in dom i & v in B9 & u = i . v ) by FUNCT_1:def 6;
hence u in N by A31, FUNCT_1:def 7; :: thesis: verum

end;

then i .: B9 c= N ;
then i .: B9 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: verum

end;

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