theorem :: FUNCT_2:60

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