theorem Th4: :: CARD_FIN:5

for X, Y being finite set
for x, y being set st ( Y is empty implies X is empty ) & not x in X & not y in Y holds
card { F where F is Function of X,Y : F is one-to-one } = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( F is one-to-one & F . x = y ) }