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