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