let n, k be Nat; :: thesis: for A, B being object st A <> B & n >= k holds
prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)
let A, B be object ; :: thesis: ( A <> B & n >= k implies prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k) )
assume A1: ( A <> B & n >= k ) ; :: thesis: prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)
then A2: card (Election (A,n,B,k)) = (n + k) choose n by Th12;
A3: ( n + k >= k + 0 & (n + k) - k = n & n + k >= n ) by NAT_1:11;
A4: (n + k) choose n > 0 by NAT_1:11, CATALAN2:26;

per cases ( n = k or n > k ) by A1, XXREAL_0:1;

suppose A5: n = k ; :: thesis: prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)

then DominatedElection (A,n,B,k) is empty by Th18;
then card (DominatedElection (A,n,B,k)) = 0 ;
then prob (DominatedElection (A,n,B,k)) = 0 / ((n + k) choose n) by A2, RPR_1:def 1;
hence prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k) by A5; :: thesis: verum

end;

suppose n > k ; :: thesis: prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)

then A6: card (DominatedElection (A,n,B,k)) = ((n - k) / (n + k)) * ((n + k) choose k) by A1, Th27
.= ((n - k) / (n + k)) * ((n + k) choose n) by A3, NEWTON:20 ;
thus prob (DominatedElection (A,n,B,k)) = (((n - k) / (n + k)) * ((n + k) choose n)) / ((n + k) choose n) by A2, A6, RPR_1:def 1
.= ((n - k) / (n + k)) * (((n + k) choose n) / ((n + k) choose n)) by XCMPLX_1:74
.= ((n - k) / (n + k)) * 1 by A4, XCMPLX_1:60
.= (n - k) / (n + k) ; :: thesis: verum

end;

end;