idseq n in Permutations n by MATRIX_2:def 11;
then {(idseq n)} in Fin (Permutations n) by Th1;
hence not for b₁ being Element of Fin (Permutations n) holds b₁ is empty ; :: thesis: verum