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 Th3;
hence card (derangements s) = round (((card s) ! ) / number_e ) by RoundCorrect; :: thesis: verum