let k be natural number ; :: thesis: Catalan (k + 1) = ((2 * k) ! ) / ((k ! ) * ((k + 1) ! ))
reconsider l = (2 * k) - k as Nat ;
( l = k & 1 * k <= 2 * k ) by XREAL_1:66;
then A1: (2 * k) choose k = ((2 * k) ! ) / ((k ! ) * (k ! )) by NEWTON:def 3;
( ((2 * k) + 2) -' 2 = 2 * k & (k + 1) -' 1 = k ) by NAT_D:34;
then Catalan (k + 1) = ((2 * k) ! ) / (((k ! ) * (k ! )) * (k + 1)) by A1, 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