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