permutations X c= Funcs (X,X) by Th2;
hence permutations X is finite ; :: thesis: verum