A1: card { F where F is Function of s,s : F is Permutation of s } = (card s) ! by CARD_FIN:8;
derangements s c= { F where F is Function of s,s : F is Permutation of s }

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in derangements s or x in { F where F is Function of s,s : F is Permutation of s } )
assume x in derangements s ; :: thesis: x in { F where F is Function of s,s : F is Permutation of s }
then ex f being Permutation of s st
( x = f & f has_no_fixpoint ) ;
hence x in { F where F is Function of s,s : F is Permutation of s } ; :: thesis: verum

end;

then card (derangements s) c= (card s) ! by A1, CARD_1:11;
hence derangements s is finite ; :: thesis: verum