let p be XFinSequence of ; :: thesis: ( rng p c= {0,1} & not p is dominated_by_0 implies ex k being Nat st
( (2 * k) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } & (2 * k) + 1 <= dom p & k = Sum (p | (2 * k)) & p . (2 * k) = 1 ) )
assume that
A1: rng p c= {0,1} and
A2: not p is dominated_by_0 ; :: thesis: ex k being Nat st
( (2 * k) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } & (2 * k) + 1 <= dom p & k = Sum (p | (2 * k)) & p . (2 * k) = 1 )
set M = { 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 x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { N where N is Element of NAT : 2 * (Sum (p | N)) > N } or x in NAT )
assume x in { N where N is Element of NAT : 2 * (Sum (p | N)) > N } ; :: thesis: x in NAT
then ex N being Element of NAT st
( x = N & 2 * (Sum (p | N)) > N ) ;
hence x in NAT ; :: thesis: verum

end;

then reconsider M = { N where N is Element of NAT : 2 * (Sum (p | N)) > N } as Subset of NAT ;
consider k being Nat such that
A3: k <= dom p and
A4: 2 * (Sum (p | k)) > k by A1, A2, Def1;
reconsider k = k as Element of NAT by ORDINAL1:def 12;
k in M by A4;
then reconsider M = M as non empty Subset of NAT ;
min* M in M by NAT_1:def 1;
then consider n being Element of NAT such that
A5: min* M = n and
A6: 2 * (Sum (p | n)) > n ;
n > 0 by A6;
then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
reconsider S = Sum (p | n1) as Element of NAT by ORDINAL1:def 12;
take S ; :: thesis: ( (2 * S) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } & (2 * S) + 1 <= dom p & S = Sum (p | (2 * S)) & p . (2 * S) = 1 )
k in M by A4;
then A7: k >= n by A5, NAT_1:def 1;
then A8: dom p >= n by A3, XXREAL_0:2;
A9: 2 * (Sum (p | n1)) = n1

proof

A10: n1 < n1 + 1 by NAT_1:13;
then n1 c= n1 + 1 by NAT_1:39;
then A11: (p | n) | n1 = p | n1 by RELAT_1:74;
( ( n = len p & p | (dom p) = p ) or n < len p ) by A8, RELAT_1:69, XXREAL_0:1;
then A12: len (p | n) = n1 + 1 by AFINSQ_1:11;
then n1 in len (p | n) by A10, NAT_1:44;
then A13: (p | n) . n1 in rng (p | n) by FUNCT_1:3;
p | n = ((p | n) | n1) ^ <%((p | n) . n1)%> by A12, AFINSQ_1:56;
then Sum (p | n) = (Sum (p | n1)) + (Sum <%((p | n) . n1)%>) by A11, AFINSQ_2:55;
then A14: (2 * (Sum (p | n1))) + (2 * (Sum <%((p | n) . n1)%>)) >= n + 1 by A6, NAT_1:13;
n1 < n1 + 1 by NAT_1:13;
then not n1 in M by A5, NAT_1:def 1;
then A15: 2 * (Sum (p | n1)) <= n1 ;
rng (p | n) c= rng p by RELAT_1:70;
then (p | n) . n1 in {0,1} by A1, A13, TARSKI:def 3;
then A16: ( (p | n) . n1 = 0 or (p | n) . n1 = 1 ) by TARSKI:def 2;
assume 2 * (Sum (p | n1)) <> n1 ; :: thesis: contradiction
then ( Sum <%((p | n) . n1)%> = (p | n) . n1 & 2 * (Sum (p | n1)) < n1 ) by A15, AFINSQ_2:53, XXREAL_0:1;
then (2 * (Sum (p | n1))) + (2 * (Sum <%((p | n) . n1)%>)) < n1 + 2 by A16, XREAL_1:8;
hence contradiction by A14; :: thesis: verum

end;

p . n1 = 1

proof

n c= len p by A8, NAT_1:39;
then A17: dom (p | n) = n1 + 1 by RELAT_1:62;
dom (p | n) = len (p | n) ;
then A18: ( Sum <%0%> = 0 & p | n = ((p | n) | n1) ^ <%((p | n) . n1)%> ) by A17, AFINSQ_1:56, AFINSQ_2:53;
assume A19: p . n1 <> 1 ; :: thesis: contradiction
A20: n1 < n1 + 1 by NAT_1:13;
then n1 < dom p by A8, XXREAL_0:2;
then A21: n1 in dom p by NAT_1:44;
n1 c= n by A20, NAT_1:39;
then A22: (p | n) | n1 = p | n1 by RELAT_1:74;
n1 in n by A20, NAT_1:44;
then n1 in (dom p) /\ n by A21, XBOOLE_0:def 4;
then A23: (p | n) . n1 = p . n1 by FUNCT_1:48;
A24: n1 < n1 + 1 by NAT_1:13;
p . n1 in rng p by A21, FUNCT_1:3;
then p . n1 = 0 by A1, A19, TARSKI:def 2;
then Sum (p | n) = (Sum (p | n1)) + 0 by A18, A23, A22, AFINSQ_2:55;
hence contradiction by A6, A9, A24; :: thesis: verum

end;

hence ( (2 * S) + 1 = min* { N where N is Element of NAT : 2 * (Sum (p | N)) > N } & (2 * S) + 1 <= dom p & S = Sum (p | (2 * S)) & p . (2 * S) = 1 ) by A3, A5, A7, A9, XXREAL_0:2; :: thesis: verum