let s be non empty finite set ; :: thesis: ex c being real number 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 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:74;
A4: Sum XF = card (derangements s) by A1, Th1;
set T = Taylor exp_R ,([#] REAL ),0 ,(- 1);
consider c being real number 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 TaylorExp;
Partial_Sums (((card s) ! ) (#) (Taylor exp_R ,([#] REAL ),0 ,(- 1))) = ((card s) ! ) (#) (Partial_Sums (Taylor exp_R ,([#] REAL ),0 ,(- 1))) by SERIES_1:12;
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:13;
(Partial_Sums (((card s) ! ) (#) (Taylor exp_R ,([#] REAL ),0 ,(- 1)))) . (card s) = Sum XF

proof

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

proof

A13: 0 in dom XF by NAT_1:45, 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:13
.= ((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
.= (((card s) ! ) * ((- 1) |^ 0 )) / (0 ! )
.= f . 0 by A3, A13, A8 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A14: for j being Element of NAT st S₁[j] holds
S₁[j + 1]

proof

let j be Element of 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 (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:45;
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:13
.= ((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
.= (((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 SERIES_1:def 1, A15, NAT_1:45, A18
.= addint . (f . j),(XF . (j + 1)) by BINOP_2:def 20
.= f . (j + 1) by A9, A17, A2 ;
:: thesis: verum

end;

for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A12, A14);
hence (Partial_Sums (((card s) ! ) (#) (Taylor exp_R ,([#] REAL ),0 ,(- 1)))) . (card s) = Sum XF by A11, A2, NAT_1:46; :: 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