let X, f be set ; :: thesis: ( f in permutations X implies f is Permutation of X )

assume f in permutations X ; :: thesis: f is Permutation of X

then ex g being Permutation of X st g = f ;

hence f is Permutation of X ; :: thesis: verum

assume f in permutations X ; :: thesis: f is Permutation of X

then ex g being Permutation of X st g = f ;

hence f is Permutation of X ; :: thesis: verum