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