let s be finite set ; :: thesis: derangements s = { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) }
set xx = { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } ;

hereby :: according to XBOOLE_0:def 10,TARSKI:def 3 :: thesis: { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } c= derangements s

let x be object ; :: thesis: ( x in derangements s implies x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } )
assume x in derangements s ; :: thesis: x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) }
then consider f being Permutation of s such that
A1: ( x = f & f is without_fixpoints ) ;
for y being set st y in s holds
f . y <> y by A1, ABIAN:def 4, ABIAN:def 5;
hence x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } by A1; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } or x in derangements s )
assume x in { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } ; :: thesis: x in derangements s
then consider h being Function of s,s such that
A2: ( x = h & h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) ;
card s = card s ;
then A3: h is onto by A2, FINSEQ_4:63;

now :: thesis: for y being object holds not y is_a_fixpoint_of h

let y be object ; :: thesis: not y is_a_fixpoint_of h
assume y is_a_fixpoint_of h ; :: thesis: contradiction
then ( y in dom h & h . y = y ) by ABIAN:def 3;
hence contradiction by A2; :: thesis: verum

end;

then h is without_fixpoints by ABIAN:def 5;
hence x in derangements s by A3, A2; :: thesis: verum