let n, k be Nat; :: thesis: for p being FinSequence of NAT holds
( p is 0 ,n,1,k -dominated-election iff ( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k & ( for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) ) )
let p be FinSequence of NAT ; :: thesis: ( p is 0 ,n,1,k -dominated-election iff ( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k & ( for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) ) )
thus ( p is 0 ,n,1,k -dominated-election implies ( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k & ( for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) ) ) :: thesis: ( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k & ( for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) implies p is 0 ,n,1,k -dominated-election )

proof

assume A1: p is 0 ,n,1,k -dominated-election ; :: thesis: ( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k & ( for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ) )
then reconsider P = p as Element of (n + k) -tuples_on {0,1} ;
A2: rng P c= {0,1} ;
then Sum p = 1 * (card (p " {1})) by Th21;
hence ( p is Tuple of n + k,{0,1} & n > 0 & Sum p = k ) by A2, A1, Th11, Th14; :: thesis: for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i
let i be Nat; :: thesis: ( i > 0 implies 2 * (Sum (p | i)) < i )
assume A3: i > 0 ; :: thesis: 2 * (Sum (p | i)) < i
rng (p | i) c= rng p by RELAT_1:70;
then A4: rng (p | i) c= {0,1} by A2;
then A5: 1 * (card ((p | i) " {1})) = Sum (p | i) by Th21;
(card ((p | i) " {1})) + (card ((p | i) " {0})) = len (p | i) by A4, Th6;
then (len (p | i)) - (Sum (p | i)) > Sum (p | i) by A1, A3, A5;
then A6: len (p | i) > (Sum (p | i)) + (Sum (p | i)) by XREAL_1:20;

per cases ( i > len p or i <= len p ) ;

suppose A7: i > len p ; :: thesis: 2 * (Sum (p | i)) < i

then p | i = p by FINSEQ_1:58;
hence 2 * (Sum (p | i)) < i by A6, A7, XXREAL_0:2; :: thesis: verum

end;

suppose i <= len p ; :: thesis: 2 * (Sum (p | i)) < i

hence 2 * (Sum (p | i)) < i by FINSEQ_1:59, A6; :: thesis: verum

end;

end;

end;

assume that
A8: p is Tuple of n + k,{0,1} and
A9: n > 0 and
A10: Sum p = k and
A11: for i being Nat st i > 0 holds
2 * (Sum (p | i)) < i ; :: thesis: p is 0 ,n,1,k -dominated-election
A12: rng p c= {0,1} by A8, FINSEQ_1:def 4;
A13: len p = n + k by A8, CARD_1:def 7;
A14: 1 * (card (p " {1})) = k by A12, Th21, A10;
reconsider P = p as Element of (n + k) -tuples_on {0,1} by A8, FINSEQ_2:92, A13;
A15: (card (p " {1})) + (card (p " {0})) = len p by A12, Th6;
then card (P " {0}) = n by A14, A13;
hence p in Election (0,n,1,k) by Def1; :: according to BALLOT_1:def 2 :: thesis: for i being Nat st i > 0 holds
card ((p | i) " {0}) > card ((p | i) " {1})
let i be Nat; :: thesis: ( i > 0 implies card ((p | i) " {0}) > card ((p | i) " {1}) )
assume A16: i > 0 ; :: thesis: card ((p | i) " {0}) > card ((p | i) " {1})
rng (p | i) c= rng p by RELAT_1:70;
then A17: rng (p | i) c= {0,1} by A12;
then A18: 1 * (card ((p | i) " {1})) = Sum (p | i) by Th21;
A19: 2 * (Sum (p | i)) < i by A16, A11;
A20: (card ((p | i) " {1})) + (card ((p | i) " {0})) = len (p | i) by A17, Th6;

per cases ( i > len p or i <= len p ) ;

suppose i > len p ; :: thesis: card ((p | i) " {0}) > card ((p | i) " {1})

then A21: p | i = p by FINSEQ_1:58;
p | (len p) = p by FINSEQ_1:58;
then 2 * (Sum p) < len p by A8, A9, A11;
then k + k < n + k by A8, A10, CARD_1:def 7;
hence card ((p | i) " {0}) > card ((p | i) " {1}) by XREAL_1:6, A14, A15, A13, A21; :: thesis: verum

end;

suppose i <= len p ; :: thesis: card ((p | i) " {0}) > card ((p | i) " {1})

then (card ((p | i) " {1})) + (card ((p | i) " {1})) < (card ((p | i) " {1})) + (card ((p | i) " {0})) by FINSEQ_1:59, A18, A20, A19;
hence card ((p | i) " {0}) > card ((p | i) " {1}) by XREAL_1:6; :: thesis: verum

end;

end;