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

proof

let x be set ; :: thesis:
assume A3: x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } ; :: thesis:
consider pN being Element of NAT ^omega such that
A4: ( pN = x & pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) by A3;
consider r2 being XFinSequence of such that
A5: pN = (pN | (2 * (k + 1))) ^ r2 by Th5;
for i being Element of NAT holds
( 2 * (k + 1) > 2 * 0 & pN is dominated_by_0 & { i : ( 2 * (Sum (pN | i)) = i & i > 0 ) } = { i : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) by A4, Th24, XREAL_1:70;
then consider r1 being XFinSequence of such that
A6: ( pN | (2 * (k + 1)) = ((1 --> 0 ) ^ r1) ^ (1 --> 1) & r1 is dominated_by_0 ) by A4, Th18;
take [r1,r2] ; :: thesis:
2 * (k + 1) > 2 * 0 by XREAL_1:70;
then reconsider M = { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } as non empty Subset of NAT by A4, NAT_1:def 1;
2 * (k + 1) in M by A4, NAT_1:def 1;
then A7: ex o being Element of NAT st
( o = 2 * (k + 1) & 2 * (Sum (pN | o)) = o & o > 0 ) ;
then ( pN is dominated_by_0 & 2 * (Sum (pN | (2 * (k + 1)))) = 2 * (k + 1) ) by A4, Th24;
then A8: ( len (pN | (2 * (k + 1))) = 2 * (k + 1) & Sum (pN | (2 * (k + 1))) = k + 1 ) by Th15;
then ( 2 * (k + 1) = (len ((1 --> 0 ) ^ r1)) + (len (1 --> 1)) & len (1 --> 1) = dom (1 --> 1) & dom (1 --> 1) = 1 ) by A6, AFINSQ_1:20, FUNCOP_1:19;
then A9: ( (2 * k) + 1 = (len (1 --> 0 )) + (len r1) & len (1 --> 0 ) = dom (1 --> 0 ) & dom (1 --> 0 ) = 1 ) by AFINSQ_1:20, FUNCOP_1:19;
( k + 1 = (Sum ((1 --> 0 ) ^ r1)) + (Sum (1 --> 1)) & Sum (1 --> 1) = 1 * 1 ) by A6, A7, Lm2, Lm4;
then ( k = (Sum (1 --> 0 )) + (Sum r1) & Sum (1 --> 0 ) = 0 * 1 ) by Lm2, Lm4;
then ( Sum r1 = k & dom r1 = 2 * k ) by A9;
then A10: r1 in Domin_0 (2 * k),k by A6, Th24;
( dom pN = n & Sum pN = m & 2 * (Sum (pN | (2 * (k + 1)))) = 2 * (k + 1) & pN is dominated_by_0 ) by A4, A7, Th24;
then ( n = (2 * (k + 1)) + (len r2) & m = (k + 1) + (Sum r2) & r2 is dominated_by_0 ) by A5, A8, Lm4, Th16, AFINSQ_1:def 4;
then ( dom r2 = j & Sum r2 = l & r2 is dominated_by_0 ) by A1;
then r2 in Domin_0 j,l by Th24;
hence ( [r1,r2] in [:(Domin_0 (2 * k),k),(Domin_0 j,l):] & S₁[x,[r1,r2]] ) by A4, A5, A6, A8, A10, 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* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } ,[:(Domin_0 (2 * k),k),(Domin_0 j,l):] such that
A11: for x being set st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } holds
S₁[x,f . x] from FUNCT_2:sch 1(A2);
A12: ( [:(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* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } = {} )

proof

assume [:(Domin_0 (2 * k),k),(Domin_0 j,l):] = {} ; :: thesis:
then ( ( Domin_0 (2 * k),k = {} or Domin_0 j,l = {} ) & Domin_0 (2 * k),k <> {} ) by Th26;
then 2 * l > j by Th26;
then (2 * m) - (2 * (k + 1)) > n - (2 * (k + 1)) by A1;
then A13: 2 * m > n by XREAL_1:11;
assume { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } <> {} ; :: thesis:
then consider x being set such that
A14: x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 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* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) by A14;
hence contradiction by A13, Th26; :: thesis:

end;

then A15: dom f = { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } by FUNCT_2:def 1;
for x, y being set st x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } & y in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } & f . x = f . y holds
x = y

proof

let x, y be set ; :: thesis:
assume that
A16: ( x in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } & y in { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } ) and
A17: f . x = f . y ; :: thesis:
consider x1, x2 being XFinSequence of such that
A18: x = (((1 --> 0 ) ^ x1) ^ (1 --> 1)) ^ x2 and
A19: ( len (((1 --> 0 ) ^ x1) ^ (1 --> 1)) = 2 * (k + 1) & f . x = [x1,x2] ) by A11, A16;
consider y1, y2 being XFinSequence of such that
A20: y = (((1 --> 0 ) ^ y1) ^ (1 --> 1)) ^ y2 and
A21: ( len (((1 --> 0 ) ^ y1) ^ (1 --> 1)) = 2 * (k + 1) & f . y = [y1,y2] ) by A11, A16;
( x1 = y1 & x2 = y2 ) by A17, A19, A21, ZFMISC_1:33;
hence x = y by A18, A20; :: thesis:

end;

then A22: f is one-to-one by A12, FUNCT_2:25;
rng f = [:(Domin_0 (2 * k),k),(Domin_0 j,l):]

proof

thus rng f c= [:(Domin_0 (2 * k),k),(Domin_0 j,l):] ; :: according to XBOOLE_0:def 10 :: thesis:
let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A23: x in [:(Domin_0 (2 * k),k),(Domin_0 j,l):] ; :: thesis:
consider x1, x2 being set such that
A24: ( x1 in Domin_0 (2 * k),k & x2 in Domin_0 j,l & x = [x1,x2] ) by A23, ZFMISC_1:def 2;
consider p being XFinSequence of such that
A25: ( p = x1 & p is dominated_by_0 & dom p = 2 * k & Sum p = k ) by A24, Def2;
consider q being XFinSequence of such that
A26: ( q = x2 & q is dominated_by_0 & dom q = j & Sum q = l ) by A24, Def2;
set 0p1 = ((1 --> 0 ) ^ p) ^ (1 --> 1);
1 <= (1 + (len p)) - (2 * (Sum p)) by A25;
then ((1 --> 0 ) ^ p) ^ (1 --> 1) is dominated_by_0 by A25, Th14;
then A27: (((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q is dominated_by_0 by A26, Th11;
( dom (((1 --> 0 ) ^ p) ^ (1 --> 1)) = (len ((1 --> 0 ) ^ p)) + (len (1 --> 1)) & len (1 --> 1) = dom (1 --> 1) & dom (1 --> 1) = 1 ) by AFINSQ_1:def 4, FUNCOP_1:19;
then A28: ( dom (((1 --> 0 ) ^ p) ^ (1 --> 1)) = ((len (1 --> 0 )) + (len p)) + 1 & len (1 --> 0 ) = dom (1 --> 0 ) & dom (1 --> 0 ) = 1 ) by AFINSQ_1:20, FUNCOP_1:19;
then A29: dom (((1 --> 0 ) ^ p) ^ (1 --> 1)) = (1 + (2 * k)) + 1 by A25;
((1 --> 0 ) ^ p) ^ (1 --> 1) = (1 --> 0 ) ^ (p ^ (1 --> 1)) by AFINSQ_1:30;
then ( Sum (((1 --> 0 ) ^ p) ^ (1 --> 1)) = (Sum (1 --> 0 )) + (Sum (p ^ (1 --> 1))) & Sum (1 --> 0 ) = 1 * 0 & Sum (1 --> 1) = 1 * 1 ) by Lm2, Lm4;
then Sum (((1 --> 0 ) ^ p) ^ (1 --> 1)) = 0 + ((Sum p) + 1) by Lm4;
then ( Sum ((((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q) = (k + 1) + l & dom ((((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q) = (len (((1 --> 0 ) ^ p) ^ (1 --> 1))) + (len q) & len (((1 --> 0 ) ^ p) ^ (1 --> 1)) = dom (((1 --> 0 ) ^ p) ^ (1 --> 1)) & len q = dom q ) by A25, A26, Lm4, AFINSQ_1:def 4;
then A30: (((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q in Domin_0 n,m by A1, A26, A27, A29, Th24;
( ((((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q) | ((2 * 1) + (len p)) = ((1 --> 0 ) ^ p) ^ (1 --> 1) & 2 * (Sum p) = len p ) by A25, A28, Th1;
then ( min* { i where i is Element of NAT : ( 2 * (Sum (((((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q) | i)) = i & i > 0 ) } = (2 * 1) + (len p) & len p = 2 * k & (((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q is Element of NAT ^omega ) by A25, Th20, AFINSQ_1:def 8;
then A31: (((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* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } by A30;
then consider r1, r2 being XFinSequence of such that
A32: ( (((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q = (((1 --> 0 ) ^ r1) ^ (1 --> 1)) ^ r2 & len (((1 --> 0 ) ^ r1) ^ (1 --> 1)) = 2 * (k + 1) & f . ((((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q) = [r1,r2] ) by A11;
dom (((1 --> 0 ) ^ r1) ^ (1 --> 1)) = 2 * (k + 1) by A32;
then ( ((((1 --> 0 ) ^ p) ^ (1 --> 1)) ^ q) | (2 * (k + 1)) = ((1 --> 0 ) ^ p) ^ (1 --> 1) & ((((1 --> 0 ) ^ r1) ^ (1 --> 1)) ^ r2) | (2 * (k + 1)) = ((1 --> 0 ) ^ r1) ^ (1 --> 1) ) by A29, Th1;
then ( (1 --> 0 ) ^ p = (1 --> 0 ) ^ r1 & q = r2 ) by A32, AFINSQ_1:31;
then ( p = r1 & q = r2 ) by AFINSQ_1:31;
hence x in rng f by A15, A24, A25, A26, A31, A32, FUNCT_1:12; :: thesis:

end;

then { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } ,[:(Domin_0 (2 * k),k),(Domin_0 j,l):] are_equipotent by A15, A22, WELLORD2:def 4;
then ( card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } = card [:(Domin_0 (2 * k),k),(Domin_0 j,l):] & card [:(Domin_0 (2 * k),k),(Domin_0 j,l):] = (card (Domin_0 (2 * k),k)) * (card (Domin_0 j,l)) ) by CARD_1:21, CARD_2:65;
hence card { pN where pN is Element of NAT ^omega : ( pN in Domin_0 n,m & 2 * (k + 1) = min* { i where i is Element of NAT : ( 2 * (Sum (pN | i)) = i & i > 0 ) } ) } = (card (Domin_0 (2 * k),k)) * (card (Domin_0 j,l)) ; :: thesis: