theorem Th5: :: TOPGEN_5:5

for a, b being set
for f being Function holds
( a in dom ((commute f) . b) iff ex g being Function st
( a in dom f & g = f . a & b in dom g ) )