let s be non empty finite set ; :: thesis: card (derangements s) = round (((card s) !) / number_e)
|.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2 by Th9;
hence card (derangements s) = round (((card s) !) / number_e) by Th4; :: thesis: verum