theorem :: PRE_CIRC:5

for I being non empty set
for A being set
for B being non-empty ManySortedSet of I
for F being ManySortedFunction of I --> A,B holds dom (commute F) = A