let k be Nat; card (Domin_0 ((6 + k),3)) = (((k + 1) * (k + 5)) * (k + 6)) / 6
card (Domin_0 ((6 + k),3)) =
((((6 + k) + 1) - (2 * 3)) / (((6 + k) + 1) - 3)) * ((6 + k) choose 3)
by Th29, NAT_1:11
.=
((k + 1) / (k + 4)) * ((((6 + k) * ((6 + k) - 1)) * ((6 + k) - 2)) / 6)
by STIRL2_1:51
.=
(((((k + 1) / (k + 4)) * (4 + k)) * (5 + k)) * (6 + k)) / 6
.=
(((k + 1) * (5 + k)) * (6 + k)) / 6
by XCMPLX_1:87
;
hence
card (Domin_0 ((6 + k),3)) = (((k + 1) * (k + 5)) * (k + 6)) / 6
; verum