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