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 set ; :: 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 has_no_fixpoint ) ;

now

let y be set ; :: thesis: ( y in s implies f . y <> y )
not y is_a_fixpoint_of f by A1, ABIAN:def 5;
hence ( y in s implies f . y <> y ) by ABIAN:def 4; :: thesis: verum

end;

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 set ; :: 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, STIRL2_1:60;

now

let y be set ; :: 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 has_no_fixpoint by ABIAN:def 5;
hence x in derangements s by A3, A2; :: thesis: verum