let n, k be Nat; for A, B being object st A <> B & n > k holds
card (DominatedElection (A,n,B,k)) = ((n - k) / (n + k)) * ((n + k) choose k)
let A, B be object ; ( A <> B & n > k implies card (DominatedElection (A,n,B,k)) = ((n - k) / (n + k)) * ((n + k) choose k) )
assume that
A1:
A <> B
and
A2:
n > k
; card (DominatedElection (A,n,B,k)) = ((n - k) / (n + k)) * ((n + k) choose k)
reconsider n1 = n - 1 as Nat by A2, NAT_1:20;
A3:
n1 + 1 = n
;
then
n1 >= k
by A2, NAT_1:13;
then A4:
n1 + k >= k + k
by XREAL_1:6;
A5:
n1 + k >= k + 0
by XREAL_1:6;
A6:
n + k >= k + 0
by XREAL_1:6;
set n1k = n1 + k;
set nk = n + k;
A7:
(n1 + k) + 1 = n + k
;
n * (1 / n) = 1
by A2, XCMPLX_1:106;
then A8: ((n + k) !) / ((n1 !) * (k !)) =
(n * (1 / n)) * (((n + k) !) / ((n1 !) * (k !)))
.=
n * ((1 / n) * (((n + k) !) / ((n1 !) * (k !))))
.=
n * (((n + k) !) / (n * ((n1 !) * (k !))))
by XCMPLX_1:103
.=
n * (((n + k) !) / ((n * (n1 !)) * (k !)))
.=
n * (((n + k) !) / ((n !) * (k !)))
by A3, NEWTON:15
;
(n + k) * (1 / (n + k)) = 1
by A2, XCMPLX_1:106;
then A9: ((n1 + k) !) / ((n1 !) * (k !)) =
((n + k) * (1 / (n + k))) * (((n1 + k) !) / ((n1 !) * (k !)))
.=
(1 / (n + k)) * ((n + k) * (((n1 + k) !) / ((n1 !) * (k !))))
.=
(1 / (n + k)) * (((n + k) * ((n1 + k) !)) / ((n1 !) * (k !)))
by XCMPLX_1:74
.=
(1 / (n + k)) * (((n + k) !) / ((n1 !) * (k !)))
by A7, NEWTON:15
.=
((1 / (n + k)) * n) * (((n + k) !) / ((n !) * (k !)))
by A8
.=
(n / (n + k)) * (((n + k) !) / ((n !) * (k !)))
by XCMPLX_1:99
;
A10:
(n1 + k) - k = n1
;
A11:
(n + k) - k = n
;
thus card (DominatedElection (A,n,B,k)) =
card (DominatedElection (0,(n1 + 1),1,k))
by A1, Th20
.=
card (Domin_0 ((n1 + k),k))
by Th26
.=
((((n1 + k) + 1) - (2 * k)) / (((n1 + k) + 1) - k)) * ((n1 + k) choose k)
by A4, CATALAN2:29
.=
((n - k) / n) * (((n1 + k) !) / ((n1 !) * (k !)))
by NEWTON:def 3, A5, A10
.=
(((n - k) / n) * (n / (n + k))) * (((n + k) !) / ((n !) * (k !)))
by A9
.=
((n - k) / (n + k)) * (((n + k) !) / ((n !) * (k !)))
by A2, XCMPLX_1:98
.=
((n - k) / (n + k)) * ((n + k) choose k)
by A11, A6, NEWTON:def 3
; verum