theorem :: CATALAN2:32

for k being Nat holds card (Domin_0 ((6 + k),3)) = (((k + 1) * (k + 5)) * (k + 6)) / 6