for P, X being set
for f being Permutation of X st P c= X holds
( f .: (f " P) = P & f " (f .: P) = P )