idseq n in Permutations n
by MATRIX_1:def 12;

then {(idseq n)} in Fin (Permutations n) by Th1;

hence not for b_{1} being Element of Fin (Permutations n) holds b_{1} is empty
; :: thesis: verum

then {(idseq n)} in Fin (Permutations n) by Th1;

hence not for b