theorem :: FUNCT_6:54

for f being Function
for x being set st x in dom (commute f) holds
(commute f) . x is Function ;