theorem Th6: :: WAYBEL27:6

for f being Function-yielding Function
for i, A being set st i in dom (commute f) holds
((commute f) . i) .: A c= pi ((f .: A),i)