for n being Nat
for f, g being Element of Permutations n holds f * g in Permutations n