for X being set
for f being Element of (SymGroup X) holds f is Permutation of X