theorem :: COUNTERS:37

for f being Function
for p being Permutation of (dom f) holds Card (f * p) = (Card f) * p