for A, B being non empty set
for C, y being set
for f being Function st f in Funcs (A,(Funcs (B,C))) & y in B holds
( dom ((commute f) . y) = A & rng ((commute f) . y) c= C )