theorem Th7: :: CARD_FIN:8

for X being finite set holds card { F where F is Function of X,X : F is Permutation of X } = (card X) !