let k be Nat; :: 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:64;
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:78
.= ((2 * k) !) / ((k !) * ((k !) * (k + 1)))
.= ((2 * k) !) / ((k !) * ((k + 1) !)) by NEWTON:15 ;
hence Catalan (k + 1) = ((2 * k) !) / ((k !) * ((k + 1) !)) ; :: thesis: verum