let s be non empty finite set ; :: thesis: ex c being Real st
( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )
set n = card s;
consider XF being XFinSequence of INT such that
A1: Sum XF = card { h where h is Function of s,s : ( h is one-to-one & ( for x being set st x in s holds
h . x <> x ) ) } and
A2: dom XF = (card s) + 1 and
A3: for m being Nat st m in dom XF holds
XF . m = (((- 1) |^ m) * ((card s) !)) / (m !) by CARD_FIN:63;
A4: Sum XF = card (derangements s) by A1, Th7;
set T = Taylor (exp_R,([#] REAL),0,(- 1));
consider c being Real such that
A5: ( c in ].(- 1),0.[ & exp_R (- 1) = ((Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) . (card s)) + (((exp_R c) * (((- 1) - 0) |^ ((card s) + 1))) / (((card s) + 1) !)) ) by Th5;
Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) = ((card s) !) (#) (Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) by SERIES_1:9;
then A6: (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card s) = ((card s) !) * ((Partial_Sums (Taylor (exp_R,([#] REAL),0,(- 1)))) . (card s)) by SEQ_1:9;
(Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card s) = Sum XF

proof

consider f being sequence of INT such that
A7: f . 0 = XF . 0 and
A8: for n being Nat st n + 1 < len XF holds
f . (n + 1) = addint . ((f . n),(XF . (n + 1))) and
A9: addint "**" XF = f . ((len XF) - 1) by A2, AFINSQ_2:def 8;
A10: Sum XF = f . ((len XF) - 1) by A9, AFINSQ_2:50;
defpred S₁[ Nat] means ( $1 in Segm ((card s) + 1) implies (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . $1 = f . $1 );
A11: 0 in REAL by XREAL_0:def 1;
A12: S₁[ 0 ]

proof

0 in Segm ((card s) + 1) by NAT_1:44;
then A13: 0 in dom XF by A2;
(Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . 0 = (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) . 0 by SERIES_1:def 1
.= ((card s) !) * ((Taylor (exp_R,([#] REAL),0,(- 1))) . 0) by SEQ_1:9
.= ((card s) !) * (((((diff (exp_R,([#] REAL))) . 0) . 0) * (((- 1) - 0) |^ 0)) / (0 !)) by TAYLOR_1:def 7
.= ((card s) !) * ((1 * ((- 1) |^ 0)) / (0 !)) by SIN_COS2:13, TAYLOR_2:7, A11
.= (((card s) !) * ((- 1) |^ 0)) / (0 !)
.= f . 0 by A3, A13, A7 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A14: for j being Nat st S₁[j] holds
S₁[j + 1]

proof

let j be Nat; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A15: S₁[j] ; :: thesis: S₁[j + 1]
set j1 = j + 1;
assume A16: j + 1 in Segm ((card s) + 1) ; :: thesis: (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (j + 1) = f . (j + 1)
then A17: j + 1 < (card s) + 1 by NAT_1:44;
then A18: j < (card s) + 1 by NAT_1:13;
(((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1)))) . (j + 1) = ((card s) !) * ((Taylor (exp_R,([#] REAL),0,(- 1))) . (j + 1)) by SEQ_1:9
.= ((card s) !) * (((((diff (exp_R,([#] REAL))) . (j + 1)) . 0) * (((- 1) - 0) |^ (j + 1))) / ((j + 1) !)) by TAYLOR_1:def 7
.= ((card s) !) * ((1 * ((- 1) |^ (j + 1))) / ((j + 1) !)) by SIN_COS2:13, TAYLOR_2:7, A11
.= (((card s) !) * ((- 1) |^ (j + 1))) / ((j + 1) !)
.= XF . (j + 1) by A3, A16, A2 ;
hence (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (j + 1) = (f . j) + (XF . (j + 1)) by A15, A18, NAT_1:44, SERIES_1:def 1
.= addint . ((f . j),(XF . (j + 1))) by BINOP_2:def 20
.= f . (j + 1) by A8, A17, A2 ;
:: thesis: verum

end;

for j being Nat holds S₁[j] from NAT_1:sch 2(A12, A14);
hence (Partial_Sums (((card s) !) (#) (Taylor (exp_R,([#] REAL),0,(- 1))))) . (card s) = Sum XF by A10, A2, NAT_1:45; :: thesis: verum

end;

then A19: (card (derangements s)) + (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) = ((card s) !) * (exp_R (- 1)) by A4, A5, A6
.= ((card s) !) * (1 / (exp_R 1)) by TAYLOR_1:4
.= ((card s) !) / number_e by IRRAT_1:def 7 ;
take c ; :: thesis: ( c in ].(- 1),0.[ & (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) )
thus c in ].(- 1),0.[ by A5; :: thesis: (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !)))
thus (card (derangements s)) - (((card s) !) / number_e) = - (((card s) !) * (((exp_R c) * ((- 1) |^ ((card s) + 1))) / (((card s) + 1) !))) by A19; :: thesis: verum