set R = RelStr(# (Bags n),() #);
set S = product (Carrier ());
set SJ = Carrier ();
set P = product ();
set J = n --> OrderedNAT;
defpred S1[ object , object ] means ( n in product (Carrier ()) & ex b being bag of n st
( b = c2 & b = n ) );
A1: for x being set st x in product (Carrier ()) 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 ()) 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 ()) ; :: 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 ()) and
A4: for y being object st y in dom (Carrier ()) holds
g . y in (Carrier ()) . 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 ; :: 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 = () . y and
A9: (Carrier ()) . 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 ; :: thesis: verum
end;
end;
A10: for x being object st x in product (Carrier ()) holds
ex y being object st S1[x,y]
proof
let x be object ; :: thesis: ( x in product (Carrier ()) implies ex y being object st S1[x,y] )
assume A11: x in product (Carrier ()) ; :: thesis: ex y being object st S1[x,y]
then consider g being Function such that
A12: x = g and
dom g = dom (Carrier ()) and
for y being object st y in dom (Carrier ()) holds
g . y in (Carrier ()) . y by CARD_3:def 5;
defpred S2[ object , object ] means c2 = g . n;
A13: for x being object st x in n holds
ex y being object st S2[x,y] ;
consider b being Function such that
A14: ( dom b = n & ( for x being object st x in n holds
S2[x,b . x] ) ) from reconsider b = b as ManySortedSet of n by ;
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:
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 ;
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: S1[x,b]
thus x in product (Carrier ()) 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 ;
hence b = x by A12; :: thesis: verum
end;
consider i being Function such that
A17: ( dom i = product (Carrier ()) & ( for x being object st x in product (Carrier ()) holds
S1[x,i . x] ) ) from A18: for x being Element of RelStr(# (Bags n),() #) ex u being Element of (product ()) st
( u in dom i & i . u = x )
proof
let x be Element of RelStr(# (Bags n),() #); :: thesis: ex u being Element of (product ()) 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 ()) holds
g . x in (Carrier ()) . x
let x be object ; :: thesis: ( x in dom (Carrier ()) implies g . x in (Carrier ()) . x )
assume x in dom (Carrier ()) ; :: thesis: g . x in (Carrier ()) . x
then A20: x in n ;
then consider L being 1-sorted such that
A21: L = () . x and
A22: (Carrier ()) . x = the carrier of L by PRALG_1:def 15;
the carrier of L = NAT by ;
hence g . x in (Carrier ()) . x by ; :: thesis: verum
end;
A23: dom g = n by PARTFUN1:def 2
.= dom (Carrier ()) by PARTFUN1:def 2 ;
then A24: g in product (Carrier ()) by ;
then reconsider g = g as Element of (product ()) by YELLOW_1:def 4;
take g ; :: thesis: ( g in dom i & i . g = x )
thus g in dom i by ; :: thesis: i . g = x
S1[g,i . g] by ;
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 ;
hence v in Bags n by ; :: thesis: verum
end;
now :: thesis: for N being Subset of RelStr(# (Bags n),() #) ex B being set st
( B is_Dickson-basis_of N, RelStr(# (Bags n),() #) & B is finite )
let N be Subset of RelStr(# (Bags n),() #); :: thesis: ex B being set st
( B is_Dickson-basis_of N, RelStr(# (Bags n),() #) & B is finite )

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

let ta, tb be Element of Bags n; :: thesis: ( a = ta & b = tb & a in product (Carrier ()) & a <= b implies ta divides tb )
assume that
A33: ( a = ta & b = tb ) and
A34: a in product (Carrier ()) ; :: 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 = () . i & ai = f . i & bi = g . i & ai <= bi ) by ;
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 = () . k and
A39: ( ak = f . k & bk = g . k ) and
A40: ak <= bk by A36;
(n --> OrderedNAT) . k = OrderedNAT by ;
then [ak,bk] in NATOrd by ;
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 ;
a9 = ak by ;
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),() #) st a in N holds
ex b being Element of RelStr(# (Bags n),() #) st
( b in i .: B9 & b <= a )
proof
let a be Element of RelStr(# (Bags n),() #); :: thesis: ( a in N implies ex b being Element of RelStr(# (Bags n),() #) st
( b in i .: B9 & b <= a ) )

consider a9 being Element of (product ()) 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 ;
assume a in N ; :: thesis: ex b being Element of RelStr(# (Bags n),() #) st
( b in i .: B9 & b <= a )

then a9 in N9 by ;
then consider b9 being Element of (product ()) such that
A48: b9 in B9 and
A49: b9 <= a9 by ;
set b = i . b9;
A50: B9 c= product (Carrier ()) by ;
then i . b9 in rng i by ;
then reconsider b = i . b9 as Element of Bags n by A25;
reconsider b = b as Element of RelStr(# (Bags n),() #) ;
take b ; :: thesis: ( b in i .: B9 & b <= a )
thus b in i .: B9 by ; :: 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 ;
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 ; :: thesis: verum
end;
then i .: B9 c= N ;
then i .: B9 is_Dickson-basis_of N, RelStr(# (Bags n),() #) by ;
hence ex B being set st
( B is_Dickson-basis_of N, RelStr(# (Bags n),() #) & B is finite ) by A30; :: thesis: verum
end;
hence RelStr(# (Bags n),() #) is Dickson by DICKSON:def 10; :: thesis: verum