for X, Y being finite set st card X <= card Y holds
card { F where F is Function of X,Y : F is one-to-one } = ((card Y) !) / (((card Y) -' (card X)) !)