for A, B being non empty set
for P being Permutation of A
for Q being Permutation of B
for f being Function of A,B holds ((P => Q) ") . f = ((Q ") * f) * P