set q1 = 1 --> 1;
set q0 = 1 --> 0;
let n, m, k, j, l be Nat; :: thesis:
assume A1: ( j = n - (2 * (k + 1)) & l = m - (k + 1) ) ; :: thesis:
defpred S₁[ object , object ] means ex r1, r2 being XFinSequence of NAT st
( $1 = (((1 --> 0) ^ r1) ^ (1 --> 1)) ^ r2 & len (((1 --> 0) ^ r1) ^ (1 --> 1)) = 2 * (k + 1) & $2 = [r1,r2] );
set Z2 = Domin_0 (j,l);
set Z1 = Domin_0 ((2 * k),k);
set F = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } ;
set 2k1 = 2 * (k + 1);
A2: for x being object st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } holds
ex y being object st
( y in [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] & S₁[x,y] )

A3: ( dom (1 --> 0) = 1 & Sum (1 --> 0) = 0 * 1 ) by AFINSQ_2:58;
let x be object ; :: thesis:
assume x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } ; :: thesis:
then consider pN being Element of NAT ^omega such that
A4: ( pN = x & pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) ;
2 * (k + 1) > 2 * 0 by XREAL_1:68;
then reconsider M = { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } as non empty Subset of NAT by A4, NAT_1:def 1;
consider r2 being XFinSequence of NAT such that
A5: pN = (pN | (2 * (k + 1))) ^ r2 by Th1;
( 2 * (k + 1) > 2 * 0 & pN is dominated_by_0 ) by A4, Th20, XREAL_1:68;
then consider r1 being XFinSequence of NAT such that
A6: pN | (2 * (k + 1)) = ((1 --> 0) ^ r1) ^ (1 --> 1) and
A7: r1 is dominated_by_0 by A4, Th14;
A8: Sum (1 --> 1) = 1 * 1 by AFINSQ_2:58;
2 * (k + 1) in M by A4, NAT_1:def 1;
then A9: ex o being Nat st
( o = 2 * (k + 1) & 2 * (Sum (pN | o)) = o & o > 0 ) ;
then k + 1 = (Sum ((1 --> 0) ^ r1)) + (Sum (1 --> 1)) by A6, AFINSQ_2:55;
then A10: k = (Sum (1 --> 0)) + (Sum r1) by A8, AFINSQ_2:55;
pN is dominated_by_0 by A4, Th20;
then A11: r2 is dominated_by_0 by A5, A9, Th12;
pN is dominated_by_0 by A4, Th20;
then A12: len (pN | (2 * (k + 1))) = 2 * (k + 1) by A9, Th11;
Sum pN = m by A4, Th20;
then A13: m = (k + 1) + (Sum r2) by A5, A9, AFINSQ_2:55;
take [r1,r2] ; :: thesis:
dom pN = n by A4, Th20;
then n = (2 * (k + 1)) + (len r2) by A5, A12, AFINSQ_1:def 3;
then A15: r2 in Domin_0 (j,l) by A1, A13, A11, Th20;
2 * (k + 1) = (len ((1 --> 0) ^ r1)) + (len (1 --> 1)) by A6, A12, AFINSQ_1:17;
then (2 * k) + 1 = (len (1 --> 0)) + (len r1) by AFINSQ_1:17;
then r1 in Domin_0 ((2 * k),k) by A7, A10, A3, Th20;
hence ( [r1,r2] in [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] & S₁[x,[r1,r2]] ) by A4, A5, A6, A12, A15, ZFMISC_1:def 2; :: thesis:

end;

consider f being Function of { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } ,[:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] such that
A16: for x being object st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
A17: ( [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] = {} implies { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } = {} )

proof

assume [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] = {} ; :: thesis:
then ( Domin_0 ((2 * k),k) = {} or Domin_0 (j,l) = {} ) ;
then 2 * l > j by Th22;
then (2 * m) - (2 * (k + 1)) > n - (2 * (k + 1)) by A1;
then A18: 2 * m > n by XREAL_1:9;
assume { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } <> {} ; :: thesis:
then consider x being object such that
A19: x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } by XBOOLE_0:def 1;
ex pN being Element of NAT ^omega st
( pN = x & pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) by A19;
hence contradiction by A18, Th22; :: thesis:

end;

then A20: dom f = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } by FUNCT_2:def 1;
A21: rng f = [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):]

proof

A22: ( Sum (1 --> 0) = 1 * 0 & Sum (1 --> 1) = 1 * 1 ) by AFINSQ_2:58;
thus rng f c= [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] ; :: according to XBOOLE_0:def 10 :: thesis:
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] ; :: thesis:
then consider x1, x2 being object such that
A24: x1 in Domin_0 ((2 * k),k) and
A25: x2 in Domin_0 (j,l) and
A26: x = [x1,x2] by ZFMISC_1:def 2;
consider p being XFinSequence of NAT such that
A27: p = x1 and
A28: p is dominated_by_0 and
A29: dom p = 2 * k and
A30: Sum p = k by A24, Def2;
consider q being XFinSequence of NAT such that
A31: q = x2 and
A32: q is dominated_by_0 and
A33: dom q = j and
A34: Sum q = l by A25, Def2;
set 0p1 = ((1 --> 0) ^ p) ^ (1 --> 1);
A35: dom ((((1 --> 0) ^ p) ^ (1 --> 1)) ^ q) = (len (((1 --> 0) ^ p) ^ (1 --> 1))) + (len q) by AFINSQ_1:def 3;
( dom (((1 --> 0) ^ p) ^ (1 --> 1)) = (len ((1 --> 0) ^ p)) + (len (1 --> 1)) & dom (1 --> 1) = 1 ) by AFINSQ_1:def 3;
then A36: dom (((1 --> 0) ^ p) ^ (1 --> 1)) = ((len (1 --> 0)) + (len p)) + 1 by AFINSQ_1:17;
then ((((1 --> 0) ^ p) ^ (1 --> 1)) ^ q) | ((2 * 1) + (len p)) = ((1 --> 0) ^ p) ^ (1 --> 1) by AFINSQ_1:57;
then A37: min* { N where N is Nat : ( 2 * (Sum (((((1 --> 0) ^ p) ^ (1 --> 1)) ^ q) | N)) = N & N > 0 ) } = (2 * 1) + (len p) by A28, A29, A30, Th16;
1 <= (1 + (len p)) - (2 * (Sum p)) by A29, A30;
then ((1 --> 0) ^ p) ^ (1 --> 1) is dominated_by_0 by A28, Th10;
then A38: (((1 --> 0) ^ p) ^ (1 --> 1)) ^ q is dominated_by_0 by A32, Th7;
A39: (((1 --> 0) ^ p) ^ (1 --> 1)) ^ q in NAT ^omega by AFINSQ_1:def 7;
((1 --> 0) ^ p) ^ (1 --> 1) = (1 --> 0) ^ (p ^ (1 --> 1)) by AFINSQ_1:27;
then Sum (((1 --> 0) ^ p) ^ (1 --> 1)) = (Sum (1 --> 0)) + (Sum (p ^ (1 --> 1))) by AFINSQ_2:55;
then Sum (((1 --> 0) ^ p) ^ (1 --> 1)) = 0 + ((Sum p) + 1) by A22, AFINSQ_2:55;
then Sum ((((1 --> 0) ^ p) ^ (1 --> 1)) ^ q) = (k + 1) + l by A30, A34, AFINSQ_2:55;
then (((1 --> 0) ^ p) ^ (1 --> 1)) ^ q in Domin_0 (n,m) by A1, A29, A33, A38, A36, A35, Th20;
then A40: (((1 --> 0) ^ p) ^ (1 --> 1)) ^ q in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } by A29, A37, A39;
then consider r1, r2 being XFinSequence of NAT such that
A41: (((1 --> 0) ^ p) ^ (1 --> 1)) ^ q = (((1 --> 0) ^ r1) ^ (1 --> 1)) ^ r2 and
A42: len (((1 --> 0) ^ r1) ^ (1 --> 1)) = 2 * (k + 1) and
A43: f . ((((1 --> 0) ^ p) ^ (1 --> 1)) ^ q) = [r1,r2] by A16;
A44: ((((1 --> 0) ^ p) ^ (1 --> 1)) ^ q) | (2 * (k + 1)) = ((1 --> 0) ^ p) ^ (1 --> 1) by A29, A36, AFINSQ_1:57;
then (1 --> 0) ^ p = (1 --> 0) ^ r1 by A41, A42, AFINSQ_1:28, AFINSQ_1:57;
then A45: p = r1 by AFINSQ_1:28;
((((1 --> 0) ^ r1) ^ (1 --> 1)) ^ r2) | (2 * (k + 1)) = ((1 --> 0) ^ r1) ^ (1 --> 1) by A42, AFINSQ_1:57;
then q = r2 by A41, A44, AFINSQ_1:28;
hence x in rng f by A20, A26, A27, A31, A40, A43, A45, FUNCT_1:3; :: thesis:

end;

for x, y being object st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } & y in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } & f . x = f . y holds
x = y

proof

let x, y be object ; :: thesis:
assume that
A46: x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } and
A47: y in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } and
A48: f . x = f . y ; :: thesis:
consider y1, y2 being XFinSequence of NAT such that
A49: y = (((1 --> 0) ^ y1) ^ (1 --> 1)) ^ y2 and
len (((1 --> 0) ^ y1) ^ (1 --> 1)) = 2 * (k + 1) and
A50: f . y = [y1,y2] by A16, A47;
consider x1, x2 being XFinSequence of NAT such that
A51: x = (((1 --> 0) ^ x1) ^ (1 --> 1)) ^ x2 and
len (((1 --> 0) ^ x1) ^ (1 --> 1)) = 2 * (k + 1) and
A52: f . x = [x1,x2] by A16, A46;
x1 = y1 by A48, A52, A50, XTUPLE_0:1;
hence x = y by A48, A51, A52, A49, A50, XTUPLE_0:1; :: thesis:

end;

then f is one-to-one by A17, FUNCT_2:19;
then { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } ,[:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] are_equipotent by A20, A21, WELLORD2:def 4;
then card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } = card [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] by CARD_1:5;
hence card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 (n,m) & 2 * (k + 1) = min* { N where N is Nat : ( 2 * (Sum (pN | N)) = N & N > 0 ) } ) } = (card (Domin_0 ((2 * k),k))) * (card (Domin_0 (j,l))) by CARD_2:46; :: thesis: