let n, k be Nat; :: thesis: for A, B being object
for f being FinSequence st f is A,n,B,k -dominated-election holds
f . 1 = A
let A, B be object ; :: thesis: for f being FinSequence st f is A,n,B,k -dominated-election holds
f . 1 = A
let f be FinSequence; :: thesis: ( f is A,n,B,k -dominated-election implies f . 1 = A )
set f1 = f | 1;
assume A1: f is A,n,B,k -dominated-election ; :: thesis: f . 1 = A
then n > k by Th14;
then len f >= 1 + 0 by A1, NAT_1:13;
then A2: len (f | 1) = 1 by FINSEQ_1:59;
card ((f | 1) " {A}) > card ((f | 1) " {B}) by A1;
then A3: not (f | 1) " {A} is empty ;
dom (f | 1) = Seg 1 by FINSEQ_1:def 3, A2;
then A4: (f | 1) " {A} = {1} by RELAT_1:132, FINSEQ_1:2, A3, ZFMISC_1:33;
1 in {1} by FINSEQ_1:2;
then (f | 1) . 1 in {A} by A4, FUNCT_1:def 7;
then A = (f | 1) . 1 by TARSKI:def 1;
hence f . 1 = A by FINSEQ_3:112; :: thesis: verum