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 such that
A1: c in ].(- 1),0.[ and
A2: (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) by Th8;
c < 0 by A1, XXREAL_1:4;
hence |.((card (derangements s)) - (((card s) !) / number_e)).| < 1 / 2 by A2, Th6; :: thesis: verum