take n --> 0 ; :: thesis: n --> 0 is n -element
thus card (n --> 0) = n by FUNCOP_1:13; :: according to CARD_1:def 6 :: thesis: verum