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_{1}[ object , object ] means ( n in product (Carrier (n --> OrderedNAT)) & ex b being bag of n st

( b = c_{2} & 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 ) )

ex y being object st S_{1}[x,y]

A17: ( dom i = product (Carrier (n --> OrderedNAT)) & ( for x being object st x in product (Carrier (n --> OrderedNAT)) holds

S_{1}[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 )

set S = product (Carrier (n --> OrderedNAT));

set SJ = Carrier (n --> OrderedNAT);

set P = product (n --> OrderedNAT);

set J = n --> OrderedNAT;

defpred S

( b = c

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

A10:
for x being object st x in product (Carrier (n --> OrderedNAT)) holds
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

end;( 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;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

ex y being object st S

proof

consider i being Function such that
let x be object ; :: thesis: ( x in product (Carrier (n --> OrderedNAT)) implies ex y being object st S_{1}[x,y] )

assume A11: x in product (Carrier (n --> OrderedNAT)) ; :: thesis: ex y being object st S_{1}[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_{2}[ object , object ] means c_{2} = g . n;

A13: for x being object st x in n holds

ex y being object st S_{2}[x,y]
;

consider b being Function such that

A14: ( dom b = n & ( for x being object st x in n holds

S_{2}[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;

then reconsider b = b as bag of n by VALUED_0:def 6;

take b ; :: thesis: S_{1}[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;assume A11: x in product (Carrier (n --> OrderedNAT)) ; :: thesis: ex y being object st S

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

A13: for x being object st x in n holds

ex y being object st S

consider b being Function such that

A14: ( dom b = n & ( for x being object st x in n holds

S

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

then
rng b c= NAT
;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;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

then reconsider b = b as bag of n by VALUED_0:def 6;

take b ; :: thesis: S

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

A17: ( dom i = product (Carrier (n --> OrderedNAT)) & ( for x being object st x in product (Carrier (n --> OrderedNAT)) holds

S

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 ;

.= 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_{1}[g,i . g]
by A17, A24;

hence i . g = x ; :: thesis: verum

end;( 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

A23: dom g =
n
by PARTFUN1:def 2
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;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

.= 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

hence i . g = x ; :: thesis: verum

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

v in Bags n

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;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

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 )

hence
RelStr(# (Bags n),(DivOrder n) #) is Dickson
by DICKSON:def 10; :: thesis: verum( 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

ex b being Element of RelStr(# (Bags n),(DivOrder n) #) st

( b in i .: B9 & b <= a )

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;( 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

A44:
for a being Element of RelStr(# (Bags n),(DivOrder n) #) st a in N holds
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;

end;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

hence
ta divides tb
by PRE_POLY:46; :: thesis: verumta . 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;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

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;( 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

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

u in N

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

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