theorem :: FUNCT_6:45

for X being set
for f being Function
for P being Permutation of X st dom f = X holds
product f, product (f * P) are_equipotent