for n being Nat
for p being Element of Permutations n holds
( p * (idseq n) = p & (idseq n) * p = p )