theorem Th109: :: FUNCT_7:110

for X being set
for p being Permutation of X
for x, y being Element of X holds (p +* (x,(p . y))) +* (y,(p . x)) is Permutation of X