theorem :: FUNCT_6:57

for A, B, C being set
for f being Function st A <> {} & B <> {} & f in Funcs (A,(Funcs (B,C))) holds
commute (commute f) = f