let X be set ; :: thesis: permutations X c= Funcs (X,X)
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in permutations X or x in Funcs (X,X) )
assume x in permutations X ; :: thesis: x in Funcs (X,X)
then x is Permutation of X by Th1;
hence x in Funcs (X,X) by FUNCT_2:9; :: thesis: verum