theorem :: CARDFIN2:15

for s being finite set holds der_seq . (card s) = card (derangements s)