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