set q1 = 1 --> 1;
set q0 = 1 --> 0;
let n, m, k, j, l be Nat; ( j = n - (2 * (k + 1)) & l = m - (k + 1) implies 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))) )
assume A1:
( j = n - (2 * (k + 1)) & l = m - (k + 1) )
; 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)))
defpred S1[ 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)):] & S1[x,y] )
proof
A3:
(
dom (1 --> 0) = 1 &
Sum (1 --> 0) = 0 * 1 )
by AFINSQ_2:58;
let x be
object ;
( 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 ) } ) } implies ex y being object st
( y in [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] & S1[x,y] ) )
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 ) } ) }
;
ex y being object st
( y in [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] & S1[x,y] )
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]
;
( [r1,r2] in [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] & S1[x,[r1,r2]] )
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)):] &
S1[
x,
[r1,r2]] )
by A4, A5, A6, A12, A15, ZFMISC_1:def 2;
verum
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
S1[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)):] = {}
;
{ 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 ) } ) } = {}
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 ) } ) } <> {}
;
contradiction
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;
verum
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)):]
;
XBOOLE_0:def 10 [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] c= rng f
let x be
object ;
TARSKI:def 3 ( not x in [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):] or x in rng f )
assume
x in [:(Domin_0 ((2 * k),k)),(Domin_0 (j,l)):]
;
x in rng f
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;
verum
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 ;
( 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 implies x = y )
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
;
x = y
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;
verum
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; verum