for k being Nat
for tr being Element of Permutations k st tr is being_transposition holds
( tr * tr = idseq k & tr = tr " )