the Permutation of X in permutations X
;

hence not permutations X is empty ; :: thesis: permutations X is functional

let x be object ; :: 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

hence not permutations X is empty ; :: thesis: permutations X is functional

let x be object ; :: 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