for D being non empty set
for F being ManySortedFunction of D
for C being non empty functional with_common_domain set st C = rng F holds
for d being Element of D
for e being set st e in DOM C holds
(F . d) . e = ((commute F) . e) . d