let p be XFinSequence of NAT ; :: 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 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 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 Nat : 2 * (Sum (p | N)) > N } ;
{ N where N is Nat : 2 * (Sum (p | N)) > N } c= NAT

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { N where N is Nat : 2 * (Sum (p | N)) > N } or x in NAT )
assume x in { N where N is Nat : 2 * (Sum (p | N)) > N } ; :: thesis: x in NAT
then ex N being Nat st
( x = N & 2 * (Sum (p | N)) > N ) ;
hence x in NAT by ORDINAL1:def 12; :: thesis: verum

end;

then reconsider M = { N where N is 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;
reconsider k = k as Nat ;
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 Nat such that
A5: min* M = n and
A6: 2 * (Sum (p | n)) > n ;
A7: Sum (p | 0) = 0 ;
Sum (p | n) > 0 by A6;
then n > 0 by A7;
then reconsider n1 = n - 1 as Nat by NAT_1:20;
reconsider S = Sum (p | n1) as Nat ;
take S ; :: thesis: ( (2 * S) + 1 = min* { N where N is 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 A8: k >= n by A5, NAT_1:def 1;
then A9: dom p >= n by A3, XXREAL_0:2;
A10: 2 * (Sum (p | n1)) = n1

proof

A11: n1 < n1 + 1 by NAT_1:13;
then Segm n1 c= Segm (n1 + 1) by NAT_1:39;
then A12: (p | n) | n1 = p | n1 by RELAT_1:74;
( ( n = len p & p | (dom p) = p ) or n < len p ) by A9, XXREAL_0:1;
then A13: len (p | n) = n1 + 1 by AFINSQ_1:11;
then n1 in Segm (len (p | n)) by A11, NAT_1:44;
then A14: (p | n) . n1 in rng (p | n) by FUNCT_1:3;
p | n = ((p | n) | n1) ^ <%((p | n) . n1)%> by A13, AFINSQ_1:56;
then Sum (p | n) = (Sum (p | n1)) + (Sum <%((p | n) . n1)%>) by A12, AFINSQ_2:55;
then A15: (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 A16: 2 * (Sum (p | n1)) <= n1 ;
(p | n) . n1 in {0,1} by A1, A14;
then A17: ( (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 A16, AFINSQ_2:53, XXREAL_0:1;
then (2 * (Sum (p | n1))) + (2 * (Sum <%((p | n) . n1)%>)) < n1 + 2 by A17, XREAL_1:8;
hence contradiction by A15; :: thesis: verum

end;

p . n1 = 1

proof

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

end;

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