let n, k be Nat; :: thesis: for d being XFinSequence of NAT holds
( d in Domin_0 ((n + k),k) iff <*0*> ^ (XFS2FS d) in DominatedElection (0,(n + 1),1,k) )
let d be XFinSequence of NAT ; :: thesis: ( d in Domin_0 ((n + k),k) iff <*0*> ^ (XFS2FS d) in DominatedElection (0,(n + 1),1,k) )
set Xd = XFS2FS d;
set Z = <*0*>;
set ZXd = <*0*> ^ (XFS2FS d);
reconsider D = d as XFinSequence of REAL ;
A1: len <*0*> = 1 by FINSEQ_1:39;
rng <*0*> = {0} by FINSEQ_1:39;
then A2: rng <*0*> c= {0,1} by ZFMISC_1:7;
thus ( d in Domin_0 ((n + k),k) implies <*0*> ^ (XFS2FS d) in DominatedElection (0,(n + 1),1,k) ) :: thesis: ( <*0*> ^ (XFS2FS d) in DominatedElection (0,(n + 1),1,k) implies d in Domin_0 ((n + k),k) )

proof

assume A4: d in Domin_0 ((n + k),k) ; :: thesis: <*0*> ^ (XFS2FS d) in DominatedElection (0,(n + 1),1,k)
then A5: d is dominated_by_0 by CATALAN2:20;
A6: Sum d = k by A4, CATALAN2:20;
len d = n + k by A4, CATALAN2:20;
then A7: len (XFS2FS d) = n + k by AFINSQ_1:def 9;
A8: rng (XFS2FS d) c= {0,1} by A5, Th2;
rng (<*0*> ^ (XFS2FS d)) = (rng <*0*>) \/ (rng (XFS2FS d)) by FINSEQ_1:31;
then reconsider ZX = <*0*> ^ (XFS2FS d) as FinSequence of {0,1} by XBOOLE_1:8, A8, A2, FINSEQ_1:def 4;
len ZX = (n + k) + 1 by A1, A7, FINSEQ_1:22;
then A9: ZX is Tuple of (n + 1) + k,{0,1} by CARD_1:def 7;
A10: Sum (<*0*> ^ (XFS2FS d)) = 0 + (Sum (XFS2FS d)) by RVSUM_1:76
.= 0 + (addreal $$ (XFS2FS D)) by RVSUM_1:def 12
.= addreal "**" D by AFINSQ_2:44
.= k by A6, AFINSQ_2:48 ;
for i being Nat st i > 0 holds
2 * (Sum ((<*0*> ^ (XFS2FS d)) | i)) < i

proof

let i be Nat; :: thesis: ( i > 0 implies 2 * (Sum ((<*0*> ^ (XFS2FS d)) | i)) < i )
assume A11: i > 0 ; :: thesis: 2 * (Sum ((<*0*> ^ (XFS2FS d)) | i)) < i
reconsider i1 = i - 1 as Nat by A11, NAT_1:14, NAT_1:21;
(<*0*> ^ (XFS2FS d)) | i = (<*0*> ^ (XFS2FS d)) | (Seg (i1 + 1))
.= <*0*> ^ ((XFS2FS d) | i1) by A1, FINSEQ_6:14 ;
then A12: Sum ((<*0*> ^ (XFS2FS d)) | i) = 0 + (Sum ((XFS2FS d) | i1)) by RVSUM_1:76
.= 0 + (Sum (XFS2FS (d | i1))) by Th1
.= Sum (XFS2FS (D | i1))
.= addreal $$ (XFS2FS (D | i1)) by RVSUM_1:def 12
.= addreal "**" (D | i1) by AFINSQ_2:44
.= Sum (d | i1) by AFINSQ_2:48 ;
2 * (Sum (d | i1)) < i1 + 1 by A5, CATALAN2:2, NAT_1:13;
hence 2 * (Sum ((<*0*> ^ (XFS2FS d)) | i)) < i by A12; :: thesis: verum

end;

then <*0*> ^ (XFS2FS d) is 0 ,n + 1,1,k -dominated-election by A9, Th22, A10;
hence <*0*> ^ (XFS2FS d) in DominatedElection (0,(n + 1),1,k) by Def3; :: thesis: verum

end;

assume <*0*> ^ (XFS2FS d) in DominatedElection (0,(n + 1),1,k) ; :: thesis: d in Domin_0 ((n + k),k)
then A13: <*0*> ^ (XFS2FS d) is 0 ,n + 1,1,k -dominated-election by Def3;
then <*0*> ^ (XFS2FS d) is Tuple of (n + 1) + k,{0,1} by Th22;
then A14: rng (<*0*> ^ (XFS2FS d)) c= {0,1} by FINSEQ_1:def 4;
rng (XFS2FS d) c= rng (<*0*> ^ (XFS2FS d)) by FINSEQ_1:30;
then A15: rng (XFS2FS d) c= {0,1} by A14;
A16: len (<*0*> ^ (XFS2FS d)) = (n + 1) + k by A13, CARD_1:def 7;
A17: len (<*0*> ^ (XFS2FS d)) = 1 + (len (XFS2FS d)) by A1, FINSEQ_1:22;
A18: len (XFS2FS d) = len d by AFINSQ_1:def 9;
for k being Nat st k <= dom d holds
2 * (Sum (d | k)) <= k

proof

let k be Nat; :: thesis: ( k <= dom d implies 2 * (Sum (d | k)) <= k )
assume k <= dom d ; :: thesis: 2 * (Sum (d | k)) <= k
(<*0*> ^ (XFS2FS d)) | (k + 1) = <*0*> ^ ((XFS2FS d) | k) by A1, FINSEQ_6:14;
then Sum ((<*0*> ^ (XFS2FS d)) | (k + 1)) = 0 + (Sum ((XFS2FS d) | k)) by RVSUM_1:76
.= 0 + (Sum (XFS2FS (d | k))) by Th1
.= Sum (XFS2FS (D | k))
.= addreal $$ (XFS2FS (D | k)) by RVSUM_1:def 12
.= addreal "**" (D | k) by AFINSQ_2:44
.= Sum (d | k) by AFINSQ_2:48 ;
then 2 * (Sum (d | k)) < k + 1 by A13, Th22;
hence 2 * (Sum (d | k)) <= k by NAT_1:13; :: thesis: verum

end;

then A19: d is dominated_by_0 by A15, Th2;
Sum (<*0*> ^ (XFS2FS d)) = 0 + (Sum (XFS2FS d)) by RVSUM_1:76
.= Sum (XFS2FS D)
.= addreal $$ (XFS2FS D) by RVSUM_1:def 12
.= addreal "**" D by AFINSQ_2:44
.= Sum d by AFINSQ_2:48 ;
then Sum d = k by A13, Th22;
hence d in Domin_0 ((n + k),k) by A19, A16, A17, A18, CATALAN2:def 2; :: thesis: verum