let s be finite set ; :: thesis: der_seq . (card s) = card (derangements s)
defpred S₁[ finite set ] means for s being finite set st card s = $1 holds
der_seq . $1 = card (derangements s);
A1: S₁[ 0 ]

proof

let s be finite set ; :: thesis: ( card s = 0 implies der_seq . 0 = card (derangements s) )
assume card s = 0 ; :: thesis: der_seq . 0 = card (derangements s)
then A2: s = {} ;
thus der_seq . 0 = 1 by Def3
.= card (derangements s) by Th11, A2, CARD_1:30 ; :: thesis: verum

end;

A3: S₁[1]

proof

let s be finite set ; :: thesis: ( card s = 1 implies der_seq . 1 = card (derangements s) )
assume card s = 1 ; :: thesis: der_seq . 1 = card (derangements s)
then consider x being object such that
A4: s = {x} by CARD_2:42;
thus der_seq . 1 = card {} by Def3
.= card (derangements s) by Th12, A4 ; :: thesis: verum

end;

A5: for n being Nat st S₁[n] & S₁[n + 1] holds
S₁[n + 2]

proof

let n be Nat; :: thesis: ( S₁[n] & S₁[n + 1] implies S₁[n + 2] )
assume A6: S₁[n] ; :: thesis: ( not S₁[n + 1] or S₁[n + 2] )
assume A7: S₁[n + 1] ; :: thesis: S₁[n + 2]
set n1 = n + 1;
A8: ( card n = n & card (n + 1) = n + 1 ) ;
then consider XFn being XFinSequence of INT such that
A9: Sum XFn = card { h where h is Function of n,n : ( h is one-to-one & ( for x being set st x in n holds
h . x <> x ) ) } and
A10: dom XFn = n + 1 and
A11: for m being Nat st m in dom XFn holds
XFn . m = (((- 1) |^ m) * (n !)) / (m !) by CARD_FIN:63;
consider XFn1 being XFinSequence of INT such that
A12: Sum XFn1 = card { h where h is Function of (n + 1),(n + 1) : ( h is one-to-one & ( for x being set st x in n + 1 holds
h . x <> x ) ) } and
A13: dom XFn1 = Segm ((n + 1) + 1) and
A14: for m being Nat st m in dom XFn1 holds
XFn1 . m = (((- 1) |^ m) * ((n + 1) !)) / (m !) by A8, CARD_FIN:63;
Sum XFn = card (derangements n) by A9, Th7;
then A15: der_seq . n = Sum XFn by A6, A8;
Sum XFn1 = card (derangements (n + 1)) by A12, Th7;
then A16: der_seq . (n + 1) = Sum XFn1 by A7, A8;
let sn2 be finite set ; :: thesis: ( card sn2 = n + 2 implies der_seq . (n + 2) = card (derangements sn2) )
assume card sn2 = n + 2 ; :: thesis: der_seq . (n + 2) = card (derangements sn2)
then consider XFn2 being XFinSequence of INT such that
A17: Sum XFn2 = card { h where h is Function of sn2,sn2 : ( h is one-to-one & ( for x being set st x in sn2 holds
h . x <> x ) ) } and
A18: dom XFn2 = Segm ((n + 2) + 1) and
A19: for m being Nat st m in dom XFn2 holds
XFn2 . m = (((- 1) |^ m) * ((n + 2) !)) / (m !) by CARD_FIN:63;
A20: Sum XFn2 = card (derangements sn2) by A17, Th7;
A21: len XFn1 = (len XFn) + 1 by A10, A13;
A22: len XFn2 = (len XFn1) + 1 by A13, A18;
n + 1 < n + 2 by XREAL_1:8;
then Segm (n + 1) c= Segm (n + 2) by NAT_1:39;
then A23: len XFn c= dom XFn1 by A10, A13;
A24: dom ((n + 1) (#) XFn) = len XFn by VALUED_1:def 5;

A25: now :: thesis: for x being object st x in dom (XFn1 | (len XFn)) holds
(XFn1 | (len XFn)) . x = ((n + 1) (#) XFn) . x

let x be object ; :: thesis: ( x in dom (XFn1 | (len XFn)) implies (XFn1 | (len XFn)) . x = ((n + 1) (#) XFn) . x )
assume A26: x in dom (XFn1 | (len XFn)) ; :: thesis: (XFn1 | (len XFn)) . x = ((n + 1) (#) XFn) . x
then A27: x in dom XFn1 by RELAT_1:57;
reconsider m = x as Element of NAT by A26;
A28: m in dom XFn by A26, RELAT_1:57;
thus (XFn1 | (len XFn)) . x = XFn1 . x by A26, FUNCT_1:47
.= (((- 1) |^ m) * ((n + 1) !)) / (m !) by A27, A14
.= (((- 1) |^ m) * ((n !) * (n + 1))) / (m !) by NEWTON:15
.= (n + 1) * ((((- 1) |^ m) * (n !)) / (m !))
.= (n + 1) * (XFn . m) by A11, A28
.= ((n + 1) (#) XFn) . x by VALUED_1:6 ; :: thesis: verum

end;

set a = (- 1) |^ (n + 1);
A29: (- 1) * ((- 1) |^ (n + 1)) = (- 1) |^ ((n + 1) + 1) by NEWTON:6;
(n + 1) + 0 < (n + 1) + 1 by XREAL_1:8;
then A30: n + 1 in dom XFn1 by A13, NAT_1:44;
(n + 2) + 0 < (n + 2) + 1 by XREAL_1:8;
then A31: n + 2 in dom XFn2 by A18, NAT_1:44;
XFn1 | (len XFn) = (n + 1) (#) XFn by A23, A24, A25, FUNCT_1:2, RELAT_1:62;
then A32: Sum XFn1 = ((n + 1) * (Sum XFn)) + (XFn1 . (len XFn)) by Th14, A21
.= ((n + 1) * (Sum XFn)) + ((((- 1) |^ (n + 1)) * ((n + 1) !)) / ((n + 1) !)) by A10, A14, A30
.= ((n + 1) * (Sum XFn)) + (((- 1) |^ (n + 1)) * (((n + 1) !) / ((n + 1) !)))
.= ((n + 1) * (Sum XFn)) + (((- 1) |^ (n + 1)) * 1) by XCMPLX_1:60 ;

A33: now :: thesis: for x being object st x in dom (XFn2 | (len XFn1)) holds
(XFn2 | (len XFn1)) . x = ((n + 2) (#) XFn1) . x

let x be object ; :: thesis: ( x in dom (XFn2 | (len XFn1)) implies (XFn2 | (len XFn1)) . x = ((n + 2) (#) XFn1) . x )
assume A34: x in dom (XFn2 | (len XFn1)) ; :: thesis: (XFn2 | (len XFn1)) . x = ((n + 2) (#) XFn1) . x
then A35: x in dom XFn2 by RELAT_1:57;
reconsider m = x as Element of NAT by A34;
A36: m in dom XFn1 by A34, RELAT_1:57;
thus (XFn2 | (len XFn1)) . x = XFn2 . x by A34, FUNCT_1:47
.= (((- 1) |^ m) * (((n + 1) + 1) !)) / (m !) by A35, A19
.= (((- 1) |^ m) * (((n + 1) !) * ((n + 1) + 1))) / (m !) by NEWTON:15
.= ((n + 1) + 1) * ((((- 1) |^ m) * ((n + 1) !)) / (m !))
.= (n + 2) * (XFn1 . m) by A14, A36
.= ((n + 2) (#) XFn1) . x by VALUED_1:6 ; :: thesis: verum

end;

n + 2 < n + 3 by XREAL_1:8;
then len XFn1 c= dom XFn2 by A13, A18, NAT_1:39;
then A37: dom (XFn2 | (len XFn1)) = len XFn1 by RELAT_1:62;
dom ((n + 2) (#) XFn1) = len XFn1 by VALUED_1:def 5;
then Sum XFn2 = ((n + 2) * (Sum XFn1)) + (XFn2 . (len XFn1)) by Th14, A22, A37, A33, FUNCT_1:2
.= ((n + 2) * (Sum XFn1)) + ((((- 1) |^ (n + 2)) * ((n + 2) !)) / ((n + 2) !)) by A19, A31, A13
.= ((n + 2) * (Sum XFn1)) + ((- ((- 1) |^ (n + 1))) * (((n + 2) !) / ((n + 2) !))) by A29
.= ((n + 2) * (Sum XFn1)) + ((- ((- 1) |^ (n + 1))) * 1) by XCMPLX_1:60
.= (n + 1) * ((Sum XFn) + (Sum XFn1)) by A32 ;
hence der_seq . (n + 2) = card (derangements sn2) by A20, Def3, A15, A16; :: thesis: verum

end;

for n being Nat holds S₁[n] from FIB_NUM:sch 1(A1, A3, A5);
hence der_seq . (card s) = card (derangements s) ; :: thesis: verum