let k be natural number ; :: thesis: Catalan (k + 1) = ((2 * k) ! ) / ((k ! ) * ((k + 1) ! ))
A1: ((2 * k) + 2) -' 2 = 2 * k by NAT_D:34;
A2: (k + 1) -' 1 = k by NAT_D:34;
reconsider l = (2 * k) - k as Nat ;
A3: l = k ;
1 * k <= 2 * k by XREAL_1:66;
then (2 * k) choose k = ((2 * k) ! ) / ((k ! ) * (k ! )) by A3, NEWTON:def 3;
then Catalan (k + 1) = ((2 * k) ! ) / (((k ! ) * (k ! )) * (k + 1)) by A1, A2, XCMPLX_1:79
.= ((2 * k) ! ) / ((k ! ) * ((k ! ) * (k + 1)))
.= ((2 * k) ! ) / ((k ! ) * ((k + 1) ! )) by NEWTON:21 ;
hence Catalan (k + 1) = ((2 * k) ! ) / ((k ! ) * ((k + 1) ! )) ; :: thesis: verum