set P = product (n --> OrderedNAT );
set J = n --> OrderedNAT ;
set S = product (Carrier (n --> OrderedNAT ));
set SJ = Carrier (n --> OrderedNAT );
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 A2: 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 ) )
let g' be Function; :: thesis: ( x = g' implies ( dom g' = n & ( for y being set st y in dom g' holds
g' . y in NAT ) ) )
assume A3: x = g' ; :: thesis: ( dom g' = n & ( for y being set st y in dom g' holds
g' . y in NAT ) )
consider g being Function such that
A4: ( x = g & dom g = dom (Carrier (n --> OrderedNAT )) & ( for y being set st y in dom (Carrier (n --> OrderedNAT )) holds
g . y in (Carrier (n --> OrderedNAT )) . y ) ) by A2, CARD_3:def 5;
thus dom g' = n by A3, A4, PARTFUN1:def 4; :: thesis: for y being set st y in dom g' holds
g' . y in NAT
thus for y being set st y in dom g' holds
g' . y in NAT :: thesis: verum

proof

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

end;

end;

defpred S₁[ set , set ] means ( n in product (Carrier (n --> OrderedNAT )) & ex b being bag of st
( b = c₂ & b = n ) );
A9: 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: ( x in product (Carrier (n --> OrderedNAT )) implies ex y being set st S₁[x,y] )
assume A10: x in product (Carrier (n --> OrderedNAT )) ; :: thesis: ex y being set st S₁[x,y]
then consider g being Function such that
A11: ( x = g & dom g = dom (Carrier (n --> OrderedNAT )) & ( for y being set st y in dom (Carrier (n --> OrderedNAT )) holds
g . y in (Carrier (n --> OrderedNAT )) . y ) ) by CARD_3:def 5;
A12: ( x = g & dom g = n & ( for y being set st y in dom g holds
g . y in NAT ) ) by A1, A10, A11;
defpred S₂[ set , set ] means c₂ = g . n;
A14: for x being set st x in n holds
ex y being set st S₂[x,y] ;
consider b being Function such that
A15: ( dom b = n & ( for x being set st x in n holds
S₂[x,b . x] ) ) from CLASSES1:sch 1(A14);
reconsider b = b as ManySortedSet of by A15, PARTFUN1:def 4, RELAT_1:def 18;

now

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

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: S₁[x,b]
thus x in product (Carrier (n --> OrderedNAT )) by A10; :: thesis: ex b being bag of st
( b = b & b = x )
take b ; :: thesis: ( b = b & b = x )
thus b = b ; :: thesis: b = x
thus b = x by A12, A15, FUNCT_1:9; :: thesis: verum

end;

consider i being Function such that
A18: ( 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(A9);
set R = RelStr(# (Bags n),(DivOrder n) #);

A19: now

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 set such that
A20: ( u in dom i & v = i . u ) by FUNCT_1:def 5;
( u in product (Carrier (n --> OrderedNAT )) & ex b being bag of st
( b = i . u & b = u ) ) by A18, A20;
hence v in Bags n by A20, POLYNOM1:def 14; :: thesis: verum

end;

A21: 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 by POLYNOM1:def 14;
A22: dom g = n by PARTFUN1:def 4
.= dom (Carrier (n --> OrderedNAT )) by PARTFUN1:def 4 ;

A23: now

let x be set ; :: 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 A24: x in n by PARTFUN1:def 4;
then consider L being 1-sorted such that
A25: ( L = (n --> OrderedNAT ) . x & (Carrier (n --> OrderedNAT )) . x = the carrier of L ) by PRALG_1:def 13;
the carrier of L = NAT by A24, A25, DICKSON:def 15, FUNCOP_1:13;
hence g . x in (Carrier (n --> OrderedNAT )) . x by A25; :: thesis: verum

end;

then A26: g in product (Carrier (n --> OrderedNAT )) by A22, 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 A18, A22, A23, CARD_3:def 5; :: thesis: i . g = x
S₁[g,i . g] by A18, A26;
then consider g' being Function such that
A27: ( g' = g & g' in product (Carrier (n --> OrderedNAT )) & ex b being bag of st
( b = i . g & b = g ) ) ;
thus i . g = x by A27; :: thesis: verum

end;

now

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 N' = i " N;
A28: i " N c= product (Carrier (n --> OrderedNAT )) by A18, 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 ) & B' is finite ) by DICKSON:def 10;
A30: ( B' c= N' & ( for a being Element of (product (n --> OrderedNAT )) st a in N' holds
ex b being Element of (product (n --> OrderedNAT )) st
( b in B' & b <= a ) ) ) by A29, DICKSON:def 9;
set B = i .: B';

now

let u be set ; :: thesis: ( u in i .: B' implies u in N )
assume u in i .: B' ; :: thesis: u in N
then consider v being set such that
A31: ( v in dom i & v in B' & u = i . v ) by FUNCT_1:def 12;
thus u in N by A30, A31, FUNCT_1:def 13; :: thesis: verum

end;

then A32: i .: B' c= N by TARSKI:def 3;
A33: 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 A34: ( a = ta & b = tb & 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 & ( 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: ( k in n implies ta . k <= tb . k )
assume A36: k in n ; :: thesis: ta . k <= tb . k
then consider R being RelStr , ak, bk being Element of R such that
A37: ( R = (n --> OrderedNAT ) . k & ak = f . k & bk = g . k & ak <= bk ) by A35;
(n --> OrderedNAT ) . k = OrderedNAT by A36, FUNCOP_1:13;
then [ak,bk] in NATOrd by A37, DICKSON:def 15, ORDERS_2:def 9;
then consider a', b' being Element of NAT such that
A38: ( [a',b'] = [ak,bk] & a' <= b' ) by DICKSON:def 14;
A39: a' = [ak,bk] `1 by A38, MCART_1:def 1
.= ak by MCART_1:def 1 ;
b' = [ak,bk] `2 by A38, MCART_1:def 2
.= bk by MCART_1:def 2 ;
hence ta . k <= tb . k by A34, A35, A37, A38, A39; :: thesis: verum

end;

hence ta divides tb by POLYNOM1:50; :: thesis: verum

end;

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: ( a in N implies ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in i .: B' & b <= a ) )
assume A40: a in N ; :: thesis: ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st
( b in i .: B' & b <= a )
consider a' being Element of (product (n --> OrderedNAT )) such that
A41: ( a' in dom i & i . a' = a ) by A21;
A42: ( a' in product (Carrier (n --> OrderedNAT )) & ex b being bag of st
( b = i . a' & b = a' ) ) by A18, A41;
a' in N' by A40, A41, FUNCT_1:def 13;
then consider b' being Element of (product (n --> OrderedNAT )) such that
A43: ( b' in B' & b' <= a' ) by A29, DICKSON:def 9;
set b = i . b';
A44: B' c= product (Carrier (n --> OrderedNAT )) by A28, A30, XBOOLE_1:1;
then consider b1 being bag of such that
A45: ( b1 = i . b' & b1 = b' ) by A18, A43;
i . b' in rng i by A18, A43, A44, FUNCT_1:def 5;
then reconsider b = i . b' as Element of Bags n by A19;
reconsider b = b as Element of RelStr(# (Bags n),(DivOrder n) #) ;
take b ; :: thesis: ( b in i .: B' & b <= a )
thus b in i .: B' by A18, A43, A44, FUNCT_1:def 12; :: thesis: b <= a
reconsider aa = a, bb = b as Element of Bags n ;
bb divides aa by A33, A41, A42, A43, A44, A45;
then [b,a] in DivOrder n by Def5;
hence b <= a by ORDERS_2:def 9; :: thesis: verum

end;

then i .: B' is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #) by A32, DICKSON:def 9;
hence ex B being set st
( B is_Dickson-basis_of N, RelStr(# (Bags n),(DivOrder n) #) & B is finite ) by A29; :: thesis: verum

end;

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