theorem Th1: :: CARD_FIN:2

for X, Y being finite set
for x, y being set st ( Y = {} implies X = {} ) & not x in X holds
card (Funcs (X,Y)) = card { F where F is Function of (X \/ {x}),(Y \/ {y}) : ( rng (F | X) c= Y & F . x = y ) }