the Permutation of X in permutations X ;
hence not permutations X is empty ; :: thesis: permutations X is functional
let x be set ; :: according to FUNCT_1:def 13 :: thesis: ( not x in permutations X or x is set )
thus ( not x in permutations X or x is set ) by Th1; :: thesis: verum