let m, n be Nat; :: thesis: ( 2 * (m + 1) <= n implies card ((Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1)))) = card (Choose (n,m,1,0)) )
defpred S1[ set , set ] means for p being XFinSequence of
for k being Nat st $1 = p & (2 * k) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } holds
ex r1, r2 being XFinSequence of st
( $2 = r1 ^ r2 & len r1 = (2 * k) + 1 & len r1 = len (p | ((2 * k) + 1)) & p = (p | ((2 * k) + 1)) ^ r2 & ( for o being Nat st o < (2 * k) + 1 holds
r1 . o = 1 - (p . o) ) );
assume A1: 2 * (m + 1) <= n ; :: thesis: card ((Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1)))) = card (Choose (n,m,1,0))
A2: card n = n by CARD_1:def 2;
A3: m <= m + m by XREAL_1:31;
m <= m + 1 by NAT_1:13;
then 2 * m <= 2 * (m + 1) by XREAL_1:64;
then 2 * m <= n by A1, XXREAL_0:2;
then m <= n by A3, XXREAL_0:2;
then (card n) choose m > 0 by A2, Th30;
then reconsider W = Choose (n,m,1,0) as non empty finite set by CARD_1:27, CARD_FIN:16;
set Z = Domin_0 (n,(m + 1));
set CH = Choose (n,(m + 1),1,0);
A4: for x being set st x in (Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1))) holds
ex y being set st
( y in W & S1[x,y] )
proof
let x be set ; :: thesis: ( x in (Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1))) implies ex y being set st
( y in W & S1[x,y] ) )
assume A5: x in (Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1))) ; :: thesis: ex y being set st
( y in W & S1[x,y] )
x in Choose (n,(m + 1),1,0) by A5, XBOOLE_0:def 5;
then consider p being XFinSequence of such that
A6: p = x and
A7: dom p = n and
A8: rng p c= {0,1} and
A9: Sum p = m + 1 by CARD_FIN:40;
not p in Domin_0 (n,(m + 1)) by A5, A6, XBOOLE_0:def 5;
then not p is dominated_by_0 by A7, A9, Def2;
then consider o being Nat such that
A10: ( (2 * o) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } & (2 * o) + 1 <= dom p & o = Sum (p | (2 * o)) & p . (2 * o) = 1 ) by A8, Th19;
set q = p | ((2 * o) + 1);
consider r2 being XFinSequence of such that
A11: p = (p | ((2 * o) + 1)) ^ r2 by Th5;
rng (p | ((2 * o) + 1)) c= rng p by RELAT_1:70;
then rng (p | ((2 * o) + 1)) c= {0,1} by A8, XBOOLE_1:1;
then consider r1 being XFinSequence of such that
A12: len (p | ((2 * o) + 1)) = len r1 and
A13: rng r1 c= {0,1} and
A14: for i being Nat st i <= len (p | ((2 * o) + 1)) holds
(Sum ((p | ((2 * o) + 1)) | i)) + (Sum (r1 | i)) = 1 * i and
A15: for i being Nat st i in len (p | ((2 * o) + 1)) holds
r1 . i = 1 - ((p | ((2 * o) + 1)) . i) by Th29;
take R = r1 ^ r2; :: thesis: ( R in W & S1[x,R] )
len p = (len r1) + (len r2) by A12, A11, AFINSQ_1:17;
then A16: dom R = n by A7, AFINSQ_1:def 3;
rng r2 c= rng p by A11, AFINSQ_1:25;
then rng r2 c= {0,1} by A8, XBOOLE_1:1;
then (rng r1) \/ (rng r2) c= {0,1} by A13, XBOOLE_1:8;
then A17: rng R c= {0,1} by AFINSQ_1:26;
( (p | ((2 * o) + 1)) | (dom (p | ((2 * o) + 1))) = p | ((2 * o) + 1) & r1 | (dom r1) = r1 ) by RELAT_1:69;
then A18: (Sum (p | ((2 * o) + 1))) + (Sum r1) = 1 * (len (p | ((2 * o) + 1))) by A12, A14;
A19: 2 * o < (2 * o) + 1 by NAT_1:13;
then 2 * o c= (2 * o) + 1 by NAT_1:39;
then A20: (p | ((2 * o) + 1)) | (2 * o) = p | (2 * o) by RELAT_1:74;
A21: (2 * o) + 1 c= dom p by A10, NAT_1:39;
then A22: dom (p | ((2 * o) + 1)) = (2 * o) + 1 by RELAT_1:62;
A23: len (p | ((2 * o) + 1)) = (2 * o) + 1 by A21, RELAT_1:62;
then A24: p | ((2 * o) + 1) = ((p | ((2 * o) + 1)) | (2 * o)) ^ <%((p | ((2 * o) + 1)) . (2 * o))%> by AFINSQ_1:56;
2 * o in (2 * o) + 1 by A19, NAT_1:44;
then (p | ((2 * o) + 1)) . (2 * o) = p . (2 * o) by A23, FUNCT_1:47;
then Sum (p | ((2 * o) + 1)) = (Sum (p | (2 * o))) + (Sum <%(p . (2 * o))%>) by A24, A20, AFINSQ_2:55;
then A25: Sum (p | ((2 * o) + 1)) = o + 1 by A10, AFINSQ_2:53;
m + 1 = (Sum (p | ((2 * o) + 1))) + (Sum r2) by A9, A11, AFINSQ_2:55;
then (Sum r1) + (Sum r2) = ((m + 1) - ((2 * o) + 1)) + (2 * o) by A18, A22, A25;
then Sum (r1 ^ r2) = m by AFINSQ_2:55;
hence R in W by A16, A17, CARD_FIN:40; :: thesis: S1[x,R]
thus S1[x,R] :: thesis: verum
proof
let p9 be XFinSequence of ; :: thesis: for k being Nat st x = p9 & (2 * k) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p9 | N)) > N } holds
ex r1, r2 being XFinSequence of st
( R = r1 ^ r2 & len r1 = (2 * k) + 1 & len r1 = len (p9 | ((2 * k) + 1)) & p9 = (p9 | ((2 * k) + 1)) ^ r2 & ( for o being Nat st o < (2 * k) + 1 holds
r1 . o = 1 - (p9 . o) ) )
let k be Nat; :: thesis: ( x = p9 & (2 * k) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p9 | N)) > N } implies ex r1, r2 being XFinSequence of st
( R = r1 ^ r2 & len r1 = (2 * k) + 1 & len r1 = len (p9 | ((2 * k) + 1)) & p9 = (p9 | ((2 * k) + 1)) ^ r2 & ( for o being Nat st o < (2 * k) + 1 holds
r1 . o = 1 - (p9 . o) ) ) )
assume A26: ( x = p9 & (2 * k) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p9 | N)) > N } ) ; :: thesis: ex r1, r2 being XFinSequence of st
( R = r1 ^ r2 & len r1 = (2 * k) + 1 & len r1 = len (p9 | ((2 * k) + 1)) & p9 = (p9 | ((2 * k) + 1)) ^ r2 & ( for o being Nat st o < (2 * k) + 1 holds
r1 . o = 1 - (p9 . o) ) )
set q9 = p9 | ((2 * k) + 1);
take r1 ; :: thesis: ex r2 being XFinSequence of st
( R = r1 ^ r2 & len r1 = (2 * k) + 1 & len r1 = len (p9 | ((2 * k) + 1)) & p9 = (p9 | ((2 * k) + 1)) ^ r2 & ( for o being Nat st o < (2 * k) + 1 holds
r1 . o = 1 - (p9 . o) ) )
take r2 ; :: thesis: ( R = r1 ^ r2 & len r1 = (2 * k) + 1 & len r1 = len (p9 | ((2 * k) + 1)) & p9 = (p9 | ((2 * k) + 1)) ^ r2 & ( for o being Nat st o < (2 * k) + 1 holds
r1 . o = 1 - (p9 . o) ) )
thus ( R = r1 ^ r2 & len r1 = (2 * k) + 1 & len r1 = len (p9 | ((2 * k) + 1)) & p9 = (p9 | ((2 * k) + 1)) ^ r2 ) by A6, A10, A12, A11, A21, A26, RELAT_1:62; :: thesis: for o being Nat st o < (2 * k) + 1 holds
r1 . o = 1 - (p9 . o)
thus for i being Nat st i < (2 * k) + 1 holds
r1 . i = 1 - (p9 . i) :: thesis: verum
proof
let i be Nat; :: thesis: ( i < (2 * k) + 1 implies r1 . i = 1 - (p9 . i) )
assume i < (2 * k) + 1 ; :: thesis: r1 . i = 1 - (p9 . i)
then A27: i in len (p | ((2 * o) + 1)) by A6, A10, A22, A26, NAT_1:44;
then r1 . i = 1 - ((p | ((2 * o) + 1)) . i) by A15;
hence r1 . i = 1 - (p9 . i) by A6, A26, A27, FUNCT_1:47; :: thesis: verum
end;
end;
end;
consider F being Function of ((Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1)))),W such that
A28: for x being set st x in (Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1))) holds
S1[x,F . x] from FUNCT_2:sch 1(A4);
 W c= rng F
proof
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in W or x in rng F )
assume x in W ; :: thesis: x in rng F
then consider p being XFinSequence of such that
A29: p = x and
A30: dom p = n and
A31: rng p c= {0,1} and
A32: Sum p = m by CARD_FIN:40;
set M = { N where N is Element of NAT : 2 * (Sum (p | N)) < N } ;
m < m + 1 by NAT_1:13;
then 2 * m < 2 * (m + 1) by XREAL_1:68;
then 2 * m < n by A1, XXREAL_0:2;
then ( 2 * (Sum (p | n)) < n & n in NAT ) by A30, A32, ORDINAL1:def 12, RELAT_1:69;
then A33: n in { N where N is Element of NAT : 2 * (Sum (p | N)) < N } ;
{ N where N is Element of NAT : 2 * (Sum (p | N)) < N } c= NAT
proof
let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in { N where N is Element of NAT : 2 * (Sum (p | N)) < N } or y in NAT )
assume y in { N where N is Element of NAT : 2 * (Sum (p | N)) < N } ; :: thesis: y in NAT
then ex i being Element of NAT st
( i = y & 2 * (Sum (p | i)) < i ) ;
hence y in NAT ; :: thesis: verum
end;
then reconsider M = { N where N is Element of NAT : 2 * (Sum (p | N)) < N } as non empty Subset of NAT by A33;
ex k being Nat st
( (2 * k) + 1 = min* M & Sum (p | ((2 * k) + 1)) = k & (2 * k) + 1 <= dom p )
proof
set mm = min* M;
min* M in M by NAT_1:def 1;
then A34: ex o being Element of NAT st
( min* M = o & 2 * (Sum (p | o)) < o ) ;
then reconsider m1 = (min* M) - 1 as Element of NAT by NAT_1:20;
A35: 2 * (Sum (p | (min* M))) < m1 + 1 by A34;
A36: m1 < m1 + 1 by NAT_1:13;
then m1 c= min* M by NAT_1:39;
then A37: (p | (min* M)) | m1 = p | m1 by RELAT_1:74;
min* M <= dom p by A30, A33, NAT_1:def 1;
then A38: min* M c= dom p by NAT_1:39;
then dom (p | (min* M)) = min* M by RELAT_1:62;
then m1 in dom (p | (min* M)) by A36, NAT_1:44;
then A39: (p | (min* M)) . m1 = p . m1 by FUNCT_1:47;
m1 < m1 + 1 by NAT_1:13;
then not m1 in M by NAT_1:def 1;
then 2 * (Sum (p | m1)) >= m1 ;
then A40: ( Sum <%(p . m1)%> = p . m1 & (2 * (Sum (p | m1))) + (2 * (p . m1)) >= m1 + 0 ) by AFINSQ_2:53, XREAL_1:7;
reconsider S = Sum (p | (min* M)) as Element of NAT by ORDINAL1:def 12;
take S ; :: thesis: ( (2 * S) + 1 = min* M & Sum (p | ((2 * S) + 1)) = S & (2 * S) + 1 <= dom p )
A41: min* M <= dom p by A30, A33, NAT_1:def 1;
len (p | (min* M)) = m1 + 1 by A38, RELAT_1:62;
then p | (min* M) = ((p | (min* M)) | m1) ^ <%((p | (min* M)) . m1)%> by AFINSQ_1:56;
then Sum (p | (min* M)) = (Sum (p | m1)) + (Sum <%(p . m1)%>) by A39, A37, AFINSQ_2:55;
hence ( (2 * S) + 1 = min* M & Sum (p | ((2 * S) + 1)) = S & (2 * S) + 1 <= dom p ) by A41, A40, A35, NAT_1:9; :: thesis: verum
end;
then consider k being Nat such that
A42: (2 * k) + 1 = min* M and
A43: Sum (p | ((2 * k) + 1)) = k and
A44: (2 * k) + 1 <= dom p ;
set k1 = (2 * k) + 1;
consider q being XFinSequence of such that
A45: p = (p | ((2 * k) + 1)) ^ q by Th5;
rng (p | ((2 * k) + 1)) c= rng p by RELAT_1:70;
then rng (p | ((2 * k) + 1)) c= {0,1} by A31, XBOOLE_1:1;
then consider r being XFinSequence of such that
A46: len r = len (p | ((2 * k) + 1)) and
A47: rng r c= {0,1} and
A48: for i being Nat st i <= len (p | ((2 * k) + 1)) holds
(Sum ((p | ((2 * k) + 1)) | i)) + (Sum (r | i)) = 1 * i and
A49: for i being Nat st i in len (p | ((2 * k) + 1)) holds
r . i = 1 - ((p | ((2 * k) + 1)) . i) by Th29;
set rq = r ^ q;
A50: dom (r ^ q) = (len (p | ((2 * k) + 1))) + (len q) by A46, AFINSQ_1:def 3;
A51: m = k + (Sum q) by A32, A43, A45, AFINSQ_2:55;
dom (r ^ q) = (len (p | ((2 * k) + 1))) + (len q) by A46, AFINSQ_1:def 3;
then A52: dom (r ^ q) = dom p by A45, AFINSQ_1:def 3;
( (p | ((2 * k) + 1)) | (dom (p | ((2 * k) + 1))) = p | ((2 * k) + 1) & r | (dom r) = r ) by RELAT_1:69;
then A53: (Sum (p | ((2 * k) + 1))) + (Sum r) = 1 * (len (p | ((2 * k) + 1))) by A46, A48;
rng q c= rng p by A45, AFINSQ_1:25;
then rng q c= {0,1} by A31, XBOOLE_1:1;
then (rng r) \/ (rng q) c= {0,1} by A47, XBOOLE_1:8;
then A54: rng (r ^ q) c= {0,1} by AFINSQ_1:26;
A55: (2 * k) + 1 c= dom p by A44, NAT_1:39;
then A56: len (p | ((2 * k) + 1)) = (2 * k) + 1 by RELAT_1:62;
then A57: (r ^ q) | ((2 * k) + 1) = r by A46, AFINSQ_1:57;
A58: ((2 * k) + 1) + 1 > (2 * k) + 1 by NAT_1:13;
then A59: (2 * k) + 1 < 2 * (Sum r) by A43, A53, A56;
A60: 2 * (Sum r) > (2 * k) + 1 by A43, A53, A56, A58;
then consider j being Nat such that
A61: ( (2 * j) + 1 = min* { N where N is Element of NAT : 2 * (Sum ((r ^ q) | N)) > N } & (2 * j) + 1 <= dom (r ^ q) & j = Sum ((r ^ q) | (2 * j)) & (r ^ q) . (2 * j) = 1 ) by A54, A57, Th6, Th19;
set j1 = (2 * j) + 1;
A62: len ((p | ((2 * k) + 1)) ^ q) = (len (p | ((2 * k) + 1))) + (len q) by AFINSQ_1:def 3;
not r ^ q is dominated_by_0 by A60, A57, Th6;
then A63: not r ^ q in Domin_0 (n,(m + 1)) by Th24;
set rqj = (r ^ q) | ((2 * j) + 1);
Sum (r ^ q) = (Sum r) + (Sum q) by AFINSQ_2:55;
then r ^ q in Choose (n,(m + 1),1,0) by A30, A43, A53, A56, A52, A54, A51, CARD_FIN:40;
then A64: r ^ q in (Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1))) by A63, XBOOLE_0:def 5;
then consider r1, r2 being XFinSequence of such that
A65: F . (r ^ q) = r1 ^ r2 and
A66: len r1 = (2 * j) + 1 and
A67: ( len r1 = len ((r ^ q) | ((2 * j) + 1)) & r ^ q = ((r ^ q) | ((2 * j) + 1)) ^ r2 ) and
A68: for i being Nat st i < (2 * j) + 1 holds
r1 . i = 1 - ((r ^ q) . i) by A28, A61;
A69: dom (r ^ q) = (len r1) + (len r2) by A67, AFINSQ_1:def 3;
then A70: len (r1 ^ r2) = len ((p | ((2 * k) + 1)) ^ q) by A50, A62, AFINSQ_1:17;
reconsider K = { N where N is Element of NAT : 2 * (Sum ((r ^ q) | N)) > N } as non empty Subset of NAT by A61, NAT_1:def 1;
(r ^ q) | ((2 * k) + 1) = r by A46, A56, AFINSQ_1:57;
then (2 * k) + 1 in K by A59;
then A71: (2 * k) + 1 >= (2 * j) + 1 by A61, NAT_1:def 1;
then (2 * j) + 1 c= (2 * k) + 1 by NAT_1:39;
then A72: (p | ((2 * k) + 1)) | ((2 * j) + 1) = p | ((2 * j) + 1) by RELAT_1:74;
(2 * j) + 1 in K by A61, NAT_1:def 1;
then A73: ex N being Element of NAT st
( N = (2 * j) + 1 & 2 * (Sum ((r ^ q) | N)) > N ) ;
(Sum ((p | ((2 * k) + 1)) | ((2 * j) + 1))) + (Sum (r | ((2 * j) + 1))) = ((2 * j) + 1) * 1 by A48, A56, A71;
then 2 * (Sum (r | ((2 * j) + 1))) = (2 * ((2 * j) + 1)) - (2 * (Sum (p | ((2 * j) + 1)))) by A72;
then ((2 * j) + 1) + (((2 * j) + 1) - (2 * (Sum (p | ((2 * j) + 1))))) > (2 * (Sum (p | ((2 * j) + 1)))) + (((2 * j) + 1) - (2 * (Sum (p | ((2 * j) + 1))))) by A46, A56, A71, A73, AFINSQ_1:58;
then (2 * j) + 1 > 2 * (Sum (p | ((2 * j) + 1))) by XREAL_1:6;
then (2 * j) + 1 in M ;
then (2 * j) + 1 >= (2 * k) + 1 by A42, NAT_1:def 1;
then A74: (2 * j) + 1 = (2 * k) + 1 by A71, XXREAL_0:1;
A75: len ((p | ((2 * k) + 1)) ^ q) = len (r ^ q) by A50, AFINSQ_1:def 3;
now
let i be Nat; :: thesis: ( i < len (r1 ^ r2) implies (r1 ^ r2) . i = ((p | ((2 * k) + 1)) ^ q) . i )
assume A76: i < len (r1 ^ r2) ; :: thesis: (r1 ^ r2) . i = ((p | ((2 * k) + 1)) ^ q) . i
now
per cases ( i < len r1 or i >= len r1 ) ;
suppose A77: i < len r1 ; :: thesis: (r1 ^ r2) . i = ((p | ((2 * k) + 1)) ^ q) . i
then A78: ( i in dom r1 & r1 . i = 1 - ((r ^ q) . i) ) by A66, A68, NAT_1:44;
A79: i in len r1 by A77, NAT_1:44;
A80: ( len r1 = len (p | ((2 * k) + 1)) & i in NAT ) by A55, A66, A74, ORDINAL1:def 12, RELAT_1:62;
then A81: r . i = 1 - ((p | ((2 * k) + 1)) . i) by A49, A79;
( ((p | ((2 * k) + 1)) ^ q) . i = (p | ((2 * k) + 1)) . i & (r ^ q) . i = r . i ) by A46, A79, A80, AFINSQ_1:def 3;
hence (r1 ^ r2) . i = ((p | ((2 * k) + 1)) ^ q) . i by A81, A78, AFINSQ_1:def 3; :: thesis: verum
end;
suppose A82: i >= len r1 ; :: thesis: (r1 ^ r2) . i = ((p | ((2 * k) + 1)) ^ q) . i
then A83: ((p | ((2 * k) + 1)) ^ q) . i = q . (i - (len r)) by A46, A56, A66, A74, A70, A76, AFINSQ_1:19;
( (r1 ^ r2) . i = r2 . (i - (len r1)) & (r ^ q) . i = q . (i - (len r)) ) by A46, A56, A66, A74, A70, A75, A76, A82, AFINSQ_1:19;
hence (r1 ^ r2) . i = ((p | ((2 * k) + 1)) ^ q) . i by A67, A70, A75, A76, A82, A83, AFINSQ_1:19; :: thesis: verum
end;
end;
end;
hence (r1 ^ r2) . i = ((p | ((2 * k) + 1)) ^ q) . i ; :: thesis: verum
end;
then A84: r1 ^ r2 = (p | ((2 * k) + 1)) ^ q by A69, A50, A62, AFINSQ_1:9, AFINSQ_1:17;
r ^ q in dom F by A64, FUNCT_2:def 1;
hence x in rng F by A29, A45, A65, A84, FUNCT_1:3; :: thesis: verum
end;
then A85: rng F = W by XBOOLE_0:def 10;
A86: F is one-to-one
proof
let x be set ; :: according to FUNCT_1:def 4 :: thesis: for b1 being set holds
( not x in proj1 F or not b1 in proj1 F or not F . x = F . b1 or x = b1 )
let y be set ; :: thesis: ( not x in proj1 F or not y in proj1 F or not F . x = F . y or x = y )
assume that
A87: x in dom F and
A88: y in dom F and
A89: F . x = F . y ; :: thesis: x = y
x in Choose (n,(m + 1),1,0) by A87, XBOOLE_0:def 5;
then consider p being XFinSequence of such that
A90: p = x and
A91: dom p = n and
A92: rng p c= {0,1} and
A93: Sum p = m + 1 by CARD_FIN:40;
not p in Domin_0 (n,(m + 1)) by A87, A90, XBOOLE_0:def 5;
then not p is dominated_by_0 by A91, A93, Def2;
then consider k1 being Nat such that
A94: ( (2 * k1) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } & (2 * k1) + 1 <= dom p & k1 = Sum (p | (2 * k1)) & p . (2 * k1) = 1 ) by A92, Th19;
y in Choose (n,(m + 1),1,0) by A88, XBOOLE_0:def 5;
then consider q being XFinSequence of such that
A95: q = y and
A96: dom q = n and
A97: rng q c= {0,1} and
A98: Sum q = m + 1 by CARD_FIN:40;
not q in Domin_0 (n,(m + 1)) by A88, A95, XBOOLE_0:def 5;
then not q is dominated_by_0 by A96, A98, Def2;
then consider k2 being Nat such that
A99: ( (2 * k2) + 1 = min* { N where N is Element of NAT : 2 * (Sum (q | N)) > N } & (2 * k2) + 1 <= dom q & k2 = Sum (q | (2 * k2)) & q . (2 * k2) = 1 ) by A97, Th19;
A100: len q = n by A96;
reconsider M = { N where N is Element of NAT : 2 * (Sum (q | N)) > N } as non empty Subset of NAT by A99, NAT_1:def 1;
set qk = q | ((2 * k2) + 1);
consider s1, s2 being XFinSequence of such that
A101: F . y = s1 ^ s2 and
A102: len s1 = (2 * k2) + 1 and
A103: len s1 = len (q | ((2 * k2) + 1)) and
A104: q = (q | ((2 * k2) + 1)) ^ s2 and
A105: for i being Nat st i < (2 * k2) + 1 holds
s1 . i = 1 - (q . i) by A28, A88, A95, A99;
A106: len q = (len (q | ((2 * k2) + 1))) + (len s2) by A104, AFINSQ_1:17;
then A107: len q = len (s1 ^ s2) by A103, AFINSQ_1:17;
reconsider K = { N where N is Element of NAT : 2 * (Sum (p | N)) > N } as non empty Subset of NAT by A94, NAT_1:def 1;
set pk = p | ((2 * k1) + 1);
consider r1, r2 being XFinSequence of such that
A108: F . x = r1 ^ r2 and
A109: len r1 = (2 * k1) + 1 and
A110: len r1 = len (p | ((2 * k1) + 1)) and
A111: p = (p | ((2 * k1) + 1)) ^ r2 and
A112: for i being Nat st i < (2 * k1) + 1 holds
r1 . i = 1 - (p . i) by A28, A87, A90, A94;
assume x <> y ; :: thesis: contradiction
then consider i being Nat such that
A113: i < len p and
A114: p . i <> q . i by A90, A91, A95, A96, A106, AFINSQ_1:9;
A115: len p = (len (p | ((2 * k1) + 1))) + (len r2) by A111, AFINSQ_1:17;
then A116: len p = len (r1 ^ r2) by A110, AFINSQ_1:17;
now
per cases ( k1 = k2 or k1 > k2 or k1 < k2 ) by XXREAL_0:1;
suppose A117: k1 = k2 ; :: thesis: contradiction
now
per cases ( i < len (p | ((2 * k1) + 1)) or i >= len (p | ((2 * k1) + 1)) ) ;
suppose A118: i < len (p | ((2 * k1) + 1)) ; :: thesis: contradiction
then i in len (p | ((2 * k1) + 1)) by NAT_1:44;
then A119: ( r1 . i = (r1 ^ r2) . i & s1 . i = (s1 ^ s2) . i ) by A109, A110, A102, A117, AFINSQ_1:def 3;
( r1 . i = 1 - (p . i) & s1 . i = 1 - (q . i) ) by A109, A110, A112, A105, A117, A118;
hence contradiction by A89, A108, A101, A114, A119; :: thesis: verum
end;
suppose A120: i >= len (p | ((2 * k1) + 1)) ; :: thesis: contradiction
then A121: (s1 ^ s2) . i = s2 . (i - (len (p | ((2 * k1) + 1)))) by A91, A109, A110, A96, A102, A107, A113, A117, AFINSQ_1:19;
( p . i = r2 . (i - (len (p | ((2 * k1) + 1)))) & q . i = s2 . (i - (len (p | ((2 * k1) + 1)))) ) by A91, A109, A110, A111, A102, A103, A104, A100, A113, A117, A120, AFINSQ_1:19;
hence contradiction by A89, A108, A110, A101, A116, A113, A114, A120, A121, AFINSQ_1:19; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
suppose A122: k1 > k2 ; :: thesis: contradiction
len s1 <= len p by A91, A96, A103, A106, NAT_1:11;
then A123: len s1 c= dom p by NAT_1:39;
2 * k2 < 2 * k1 by A122, XREAL_1:68;
then A124: len s1 < len r1 by A109, A102, XREAL_1:6;
then (s1 ^ s2) | (len s1) = r1 | (len s1) by A89, A108, A101, AFINSQ_1:58;
then A125: s1 = r1 | (len s1) by AFINSQ_1:57;
A126: for k being Nat st k < len (q | ((2 * k2) + 1)) holds
(q | ((2 * k2) + 1)) . k = (p | (len (q | ((2 * k2) + 1)))) . k
proof
let k be Nat; :: thesis: ( k < len (q | ((2 * k2) + 1)) implies (q | ((2 * k2) + 1)) . k = (p | (len (q | ((2 * k2) + 1)))) . k )
assume A127: k < len (q | ((2 * k2) + 1)) ; :: thesis: (q | ((2 * k2) + 1)) . k = (p | (len (q | ((2 * k2) + 1)))) . k
A128: k in len s1 by A103, A127, NAT_1:44;
then A129: k in (dom q) /\ (len s1) by A91, A96, A123, XBOOLE_0:def 4;
k in (dom p) /\ (len s1) by A123, A128, XBOOLE_0:def 4;
then A130: p . k = (p | (len (q | ((2 * k2) + 1)))) . k by A103, FUNCT_1:48;
A131: k < len r1 by A103, A124, A127, XXREAL_0:2;
then A132: r1 . k = 1 - (p . k) by A109, A112;
k in dom r1 by A131, NAT_1:44;
then k in (dom r1) /\ (len s1) by A128, XBOOLE_0:def 4;
then A133: r1 . k = (r1 | (len s1)) . k by FUNCT_1:48;
s1 . k = 1 - (q . k) by A102, A103, A105, A127;
hence (q | ((2 * k2) + 1)) . k = (p | (len (q | ((2 * k2) + 1)))) . k by A102, A125, A132, A133, A129, A130, FUNCT_1:48; :: thesis: verum
end;
(2 * k2) + 1 in M by A99, NAT_1:def 1;
then A134: ex N being Element of NAT st
( (2 * k2) + 1 = N & 2 * (Sum (q | N)) > N ) ;
len (q | ((2 * k2) + 1)) = len (p | (len (q | ((2 * k2) + 1)))) by A103, A123, RELAT_1:62;
then q | ((2 * k2) + 1) = p | (len (q | ((2 * k2) + 1))) by A126, AFINSQ_1:9;
then len (q | ((2 * k2) + 1)) in K by A102, A103, A134;
hence contradiction by A94, A109, A103, A124, NAT_1:def 1; :: thesis: verum
end;
suppose A135: k1 < k2 ; :: thesis: contradiction
len r1 <= len q by A91, A110, A96, A115, NAT_1:11;
then A136: len r1 c= dom q by NAT_1:39;
2 * k1 < 2 * k2 by A135, XREAL_1:68;
then A137: len r1 < len s1 by A109, A102, XREAL_1:6;
then (r1 ^ r2) | (len r1) = s1 | (len r1) by A89, A108, A101, AFINSQ_1:58;
then A138: r1 = s1 | (len r1) by AFINSQ_1:57;
A139: for k being Nat st k < len (p | ((2 * k1) + 1)) holds
(p | ((2 * k1) + 1)) . k = (q | (len (p | ((2 * k1) + 1)))) . k
proof
let k be Nat; :: thesis: ( k < len (p | ((2 * k1) + 1)) implies (p | ((2 * k1) + 1)) . k = (q | (len (p | ((2 * k1) + 1)))) . k )
assume A140: k < len (p | ((2 * k1) + 1)) ; :: thesis: (p | ((2 * k1) + 1)) . k = (q | (len (p | ((2 * k1) + 1)))) . k
A141: k in len r1 by A110, A140, NAT_1:44;
then A142: k in (dom p) /\ (len r1) by A91, A96, A136, XBOOLE_0:def 4;
k in (dom q) /\ (len r1) by A136, A141, XBOOLE_0:def 4;
then A143: q . k = (q | (len (p | ((2 * k1) + 1)))) . k by A110, FUNCT_1:48;
A144: k < len s1 by A110, A137, A140, XXREAL_0:2;
then A145: s1 . k = 1 - (q . k) by A102, A105;
k in dom s1 by A144, NAT_1:44;
then k in (dom s1) /\ (len r1) by A141, XBOOLE_0:def 4;
then A146: s1 . k = (s1 | (len r1)) . k by FUNCT_1:48;
r1 . k = 1 - (p . k) by A109, A110, A112, A140;
hence (p | ((2 * k1) + 1)) . k = (q | (len (p | ((2 * k1) + 1)))) . k by A109, A138, A145, A146, A142, A143, FUNCT_1:48; :: thesis: verum
end;
(2 * k1) + 1 in K by A94, NAT_1:def 1;
then A147: ex N being Element of NAT st
( (2 * k1) + 1 = N & 2 * (Sum (p | N)) > N ) ;
len (p | ((2 * k1) + 1)) = len (q | (len (p | ((2 * k1) + 1)))) by A110, A136, RELAT_1:62;
then p | ((2 * k1) + 1) = q | (len (p | ((2 * k1) + 1))) by A139, AFINSQ_1:9;
then len (p | ((2 * k1) + 1)) in M by A109, A110, A147;
hence contradiction by A110, A99, A102, A137, NAT_1:def 1; :: thesis: verum
end;
end;
end;
hence contradiction ; :: thesis: verum
end;
dom F = (Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1))) by FUNCT_2:def 1;
then (Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1))),W are_equipotent by A86, A85, WELLORD2:def 4;
hence card ((Choose (n,(m + 1),1,0)) \ (Domin_0 (n,(m + 1)))) = card (Choose (n,m,1,0)) by CARD_1:5; :: thesis: verum