theorem :: CARD_1:64

for x being object
for k being Nat holds card (k --> x) = k