theorem :: FUNCT_2:59

for X being set
for f, g being Permutation of X st g * f = g holds
f = id X