let p be XFinSequence of ; :: thesis: ( rng p c= {0 ,1} & not p is dominated_by_0 implies ex k being Element of 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 Element of 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 A3: x in { n where n is Element of NAT : 2 * (Sum (p | n)) > n } ; :: thesis: x in NAT
ex n being Element of NAT st
( x = n & 2 * (Sum (p | n)) > n ) by A3;
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 Element of NAT such that
A4: ( k <= dom p & 2 * (Sum (p | k)) > k ) by A1, A2, Def1;
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 & 2 * (Sum (p | n)) > n ) ;
n > 0

proof

assume n <= 0 ; :: thesis: contradiction
then n = 0 ;
then ( p | n = {} & dom {} = {} & len {} = dom {} ) ;
then addnat "**" (p | n) = the_unity_wrt addnat by STIRL2_1:def 3;
hence contradiction by A5, BINOP_2:5; :: thesis: verum

end;

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
take Sum (p | n1) ; :: thesis: ( (2 * (Sum (p | n1))) + 1 = min* { n where n is Element of NAT : 2 * (Sum (p | n)) > n } & (2 * (Sum (p | n1))) + 1 <= dom p & Sum (p | n1) = Sum (p | (2 * (Sum (p | n1)))) & p . (2 * (Sum (p | n1))) = 1 )
k in M by A4;
then A6: k >= n by A5, NAT_1:def 1;
then A7: dom p >= n by A4, XXREAL_0:2;
A8: 2 * (Sum (p | n1)) = n1

proof

assume A9: 2 * (Sum (p | n1)) <> n1 ; :: thesis: contradiction
n1 < n1 + 1 by NAT_1:13;
then ( not n1 in M & n1 < dom p ) by A5, A7, NAT_1:def 1, XXREAL_0:2;
then A10: ( 2 * (Sum (p | n1)) <= n1 & n1 < len p ) ;
then n1 + 1 <= len p by NAT_1:13;
then ( ( ( n = len p & p | (dom p) = p ) or n < len p ) & dom p = len p & n1 < n1 + 1 ) by NAT_1:13, RELAT_1:98, XXREAL_0:1;
then A11: ( len (p | n) = n1 + 1 & n1 c= n1 + 1 & n1 < n ) by AFINSQ_1:14, NAT_1:40;
then A12: ( p | n = ((p | n) | n1) ^ <%((p | n) . n1)%> & (p | n) | n1 = p | n1 ) by CARD_FIN:43, RELAT_1:103;
( n1 in len (p | n) & len (p | n) = dom (p | n) ) by A11, NAT_1:45;
then ( (p | n) . n1 in rng (p | n) & rng (p | n) c= rng p ) by FUNCT_1:12, RELAT_1:99;
then (p | n) . n1 in {0 ,1} by A1, TARSKI:def 3;
then ( ( (p | n) . n1 = 0 or (p | n) . n1 = 1 ) & Sum <%((p | n) . n1)%> = (p | n) . n1 & 2 * (Sum (p | n1)) < n1 ) by A9, A10, STIRL2_1:44, TARSKI:def 2, XXREAL_0:1;
then A13: (2 * (Sum (p | n1))) + (2 * (Sum <%((p | n) . n1)%>)) < n1 + 2 by XREAL_1:10;
Sum (p | n) = (Sum (p | n1)) + (Sum <%((p | n) . n1)%>) by A12, Lm4;
then (2 * (Sum (p | n1))) + (2 * (Sum <%((p | n) . n1)%>)) >= n + 1 by A5, NAT_1:13;
hence contradiction by A13; :: thesis: verum

end;

p . n1 = 1

proof

assume A14: p . n1 <> 1 ; :: thesis: contradiction
n1 < n1 + 1 by NAT_1:13;
then A15: ( n1 < dom p & n1 c= n & n1 in n & n <= len p ) by A7, NAT_1:40, NAT_1:45, XXREAL_0:2;
then ( n1 in dom p & n c= len p & len p = dom p ) by NAT_1:40, NAT_1:45;
then ( p . n1 in rng p & n1 in (dom p) /\ n & dom (p | n) = n1 + 1 & dom (p | n) = len (p | n) ) by A15, FUNCT_1:12, RELAT_1:91, XBOOLE_0:def 4;
then ( p . n1 = 0 & Sum <%0 %> = 0 & p | n = ((p | n) | n1) ^ <%((p | n) . n1)%> & (p | n) . n1 = p . n1 & (p | n) | n1 = p | n1 ) by A1, A14, A15, CARD_FIN:43, FUNCT_1:71, RELAT_1:103, STIRL2_1:44, TARSKI:def 2;
then ( Sum (p | n) = (Sum (p | n1)) + 0 & n1 < n1 + 1 ) by Lm4, NAT_1:13;
hence contradiction by A5, A8; :: thesis: verum

end;

hence ( (2 * (Sum (p | n1))) + 1 = min* { n where n is Element of NAT : 2 * (Sum (p | n)) > n } & (2 * (Sum (p | n1))) + 1 <= dom p & Sum (p | n1) = Sum (p | (2 * (Sum (p | n1)))) & p . (2 * (Sum (p | n1))) = 1 ) by A4, A5, A6, A8, XXREAL_0:2; :: thesis: verum