let X be set ; :: thesis: for f being Element of (SymGroup X) holds f is Permutation of X
let f be Element of (SymGroup X); :: thesis: f is Permutation of X
the carrier of (SymGroup X) = permutations X by Def2;
hence f is Permutation of X by Th1; :: thesis: verum