for k being Nat
for p being Element of Permutations (k + 1) st p . (k + 1) <> k + 1 holds
ex tr being Element of Permutations (k + 1) st
( tr is being_transposition & tr . (p . (k + 1)) = k + 1 & (tr * p) . (k + 1) = k + 1 )