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

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