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