theorem Th7: :: CARDFIN2:7

for s being finite set holds 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 ) ) }