theorem :: CARD_3:2

for X, Y being set holds Card (X --> Y) = X --> (card Y)