:: deftheorem Def3 defines commuting WAYBEL27:def 3 :
for F being Function holds
( F is commuting iff ( ( for x being set st x in dom F holds
x is Function-yielding Function ) & ( for f being Function st f in dom F holds
F . f = commute f ) ) );