let n be Nat; :: thesis: card (Domin_0 (n,0)) = 1
Domin_0 (n,0) = {(n --> 0)} by Th23;
hence card (Domin_0 (n,0)) = 1 by CARD_1:30; :: thesis: verum