let n be Element of NAT ; :: thesis: card (Domin_0 n,0 ) = 1
Domin_0 n,0 = {(n --> 0 )} by Th27;
hence card (Domin_0 n,0 ) = 1 by CARD_1:50; :: thesis: verum