let n be Element of NAT ; :: thesis: card (Domin_0 (2 * n),n) = Catalan (n + 1)
( ((2 * n) + 2) -' 2 = ((2 * n) + 2) - 2 & (n + 1) -' 1 = (n + 1) - 1 ) by XREAL_0:def 2;
then ( (2 * (n + 1)) -' 2 = 2 * n & (n + 1) -' 1 = n & Catalan (n + 1) = (((2 * (n + 1)) -' 2) choose ((n + 1) -' 1)) / (n + 1) ) by CATALAN1:def 1;
hence card (Domin_0 (2 * n),n) = Catalan (n + 1) by Th37; :: thesis: verum