let n be Nat; :: thesis: card (Domin_0 ((2 * n),n)) = ((2 * n) choose n) / (n + 1)
card (Domin_0 ((2 * n),n)) = ((((2 * n) + 1) - (2 * n)) / (((2 * n) + 1) - n)) * ((2 * n) choose n) by Th29
.= (1 * ((2 * n) choose n)) / (n + 1) by XCMPLX_1:74 ;
hence card (Domin_0 ((2 * n),n)) = ((2 * n) choose n) / (n + 1) ; :: thesis: verum