for x being object
for X being set
for p, q being Permutation of X
for p1, q1 being Permutation of (X \/ {x}) st p1 | X = p & q1 | X = q & p1 . x = x & q1 . x = x holds
( (p1 * q1) | X = p * q & (p1 * q1) . x = x )