let s be non empty finite set ; :: thesis: |.((card (derangements s)) - (((card s) ! ) / number_e )).| < 1 / 2
set n = card s;
consider c being real number such that
A: c in ].(- 1),0 .[ and
B: (card (derangements s)) - (((card s) ! ) / number_e ) = - (((card s) ! ) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) ! ))) by Th2;
c < 0 by A, XXREAL_1:4;
hence |.((card (derangements s)) - (((card s) ! ) / number_e )).| < 1 / 2 by B, TaylorExpRest; :: thesis: verum