theorem DR: :: NEWTON04:9

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