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 Th5, A2, CARD_1:50 ; :: 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 set such that
A4: s = {x} by CARD_2:60;
thus der_seq . 1 = card {} by Def3
.= card (derangements s) by Th6, 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 Z0: S₁[n] ; :: thesis: ( not S₁[n + 1] or S₁[n + 2] )
assume Z1: S₁[n + 1] ; :: thesis: S₁[n + 2]
set n1 = n + 1;
Z2: ( card n = n & card (n + 1) = n + 1 ) by CARD_1:def 5;
then consider XFn being XFinSequence of such that
B1: 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
B2: dom XFn = n + 1 and
B3: for m being Nat st m in dom XFn holds
XFn . m = (((- 1) |^ m) * (n !)) / (m !) by CARD_FIN:74;
consider XFn1 being XFinSequence of such that
B4: 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
B5: dom XFn1 = (n + 1) + 1 and
B6: for m being Nat st m in dom XFn1 holds
XFn1 . m = (((- 1) |^ m) * ((n + 1) !)) / (m !) by CARD_FIN:74, Z2;
Sum XFn = card (derangements n) by B1, Th1;
then B7: der_seq . n = Sum XFn by Z0, Z2;
Sum XFn1 = card (derangements (n + 1)) by B4, Th1;
then B8: der_seq . (n + 1) = Sum XFn1 by Z1, Z2;
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 such that
B9: 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
BA: dom XFn2 = (n + 2) + 1 and
BB: for m being Nat st m in dom XFn2 holds
XFn2 . m = (((- 1) |^ m) * ((n + 2) !)) / (m !) by CARD_FIN:74;
BC: Sum XFn2 = card (derangements sn2) by B9, Th1;
CA: len XFn1 = (len XFn) + 1 by B2, B5;
CAA: len XFn2 = (len XFn1) + 1 by B5, BA;
n + 1 < n + 2 by XREAL_1:10;
then CB: len XFn c= dom XFn1 by B2, B5, NAT_1:40;
CC: dom ((n + 1) (#) XFn) = len XFn by VALUED_1:def 5;

D0: now

let x be set ; :: thesis: ( x in dom (XFn1 | (len XFn)) implies (XFn1 | (len XFn)) . x = ((n + 1) (#) XFn) . x )
assume CD: x in dom (XFn1 | (len XFn)) ; :: thesis: (XFn1 | (len XFn)) . x = ((n + 1) (#) XFn) . x
then CE: x in dom XFn1 by RELAT_1:86;
reconsider m = x as Element of NAT by CD;
CF: m in dom XFn by CD, RELAT_1:86;
thus (XFn1 | (len XFn)) . x = XFn1 . x by FUNCT_1:70, CD
.= (((- 1) |^ m) * ((n + 1) !)) / (m !) by CE, B6
.= (((- 1) |^ m) * ((n !) * (n + 1))) / (m !) by NEWTON:21
.= (n + 1) * ((((- 1) |^ m) * (n !)) / (m !))
.= (n + 1) * (XFn . m) by B3, CF
.= ((n + 1) (#) XFn) . x by VALUED_1:6 ; :: thesis: verum

end;

set a = (- 1) |^ (n + 1);
D21: (- 1) * ((- 1) |^ (n + 1)) = (- 1) |^ ((n + 1) + 1) by NEWTON:11;
(n + 1) + 0 < (n + 1) + 1 by XREAL_1:10;
then D3: n + 1 in dom XFn1 by B5, NAT_1:45;
(n + 2) + 0 < (n + 2) + 1 by XREAL_1:10;
then D4: n + 2 in dom XFn2 by BA, NAT_1:45;
XFn1 | (len XFn) = (n + 1) (#) XFn by CB, CC, FUNCT_1:9, D0, RELAT_1:91;
then DA: Sum XFn1 = ((n + 1) * (Sum XFn)) + (XFn1 . (len XFn)) by Th7, CA
.= ((n + 1) * (Sum XFn)) + ((((- 1) |^ (n + 1)) * ((n + 1) !)) / ((n + 1) !)) by B2, B6, D3
.= ((n + 1) * (Sum XFn)) + (((- 1) |^ (n + 1)) * (((n + 1) !) / ((n + 1) !)))
.= ((n + 1) * (Sum XFn)) + (((- 1) |^ (n + 1)) * 1) by XCMPLX_1:60 ;

E0: now

let x be set ; :: thesis: ( x in dom (XFn2 | (len XFn1)) implies (XFn2 | (len XFn1)) . x = ((n + 2) (#) XFn1) . x )
assume CD: x in dom (XFn2 | (len XFn1)) ; :: thesis: (XFn2 | (len XFn1)) . x = ((n + 2) (#) XFn1) . x
then CE: x in dom XFn2 by RELAT_1:86;
reconsider m = x as Element of NAT by CD;
CF: m in dom XFn1 by CD, RELAT_1:86;
thus (XFn2 | (len XFn1)) . x = XFn2 . x by FUNCT_1:70, CD
.= (((- 1) |^ m) * (((n + 1) + 1) !)) / (m !) by CE, BB
.= (((- 1) |^ m) * (((n + 1) !) * ((n + 1) + 1))) / (m !) by NEWTON:21
.= ((n + 1) + 1) * ((((- 1) |^ m) * ((n + 1) !)) / (m !))
.= (n + 2) * (XFn1 . m) by B6, CF
.= ((n + 2) (#) XFn1) . x by VALUED_1:6 ; :: thesis: verum

end;

n + 2 < n + 3 by XREAL_1:10;
then len XFn1 c= dom XFn2 by B5, BA, NAT_1:40;
then EB: dom (XFn2 | (len XFn1)) = len XFn1 by RELAT_1:91;
dom ((n + 2) (#) XFn1) = len XFn1 by VALUED_1:def 5;
then Sum XFn2 = ((n + 2) * (Sum XFn1)) + (XFn2 . (len XFn1)) by Th7, CAA, EB, FUNCT_1:9, E0
.= ((n + 2) * (Sum XFn1)) + ((((- 1) |^ (n + 2)) * ((n + 2) !)) / ((n + 2) !)) by BB, D4, B5
.= ((n + 2) * (Sum XFn1)) + ((- ((- 1) |^ (n + 1))) * (((n + 2) !) / ((n + 2) !))) by D21
.= ((n + 2) * (Sum XFn1)) + ((- ((- 1) |^ (n + 1))) * 1) by XCMPLX_1:60
.= (n + 1) * ((Sum XFn) + (Sum XFn1)) by DA ;
hence der_seq . (n + 2) = card (derangements sn2) by BC, Def3, B7, B8; :: 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