theorem :: FUNCT_7:111

for f being Function
for x, y being set st x in dom f & y in dom f holds
ex p being Permutation of (dom f) st (f +* (x,(f . y))) +* (y,(f . x)) = f * p