theorem Th4: :: GR_FREE0:4

for f being Function
for x being object st x in dom f holds
(commute <*f*>) . x = <*(f . x)*>