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