theorem :: CATALAN2:31

for k being Nat holds card (Domin_0 ((4 + k),2)) = ((k + 1) * (k + 4)) / 2