theorem :: PRALG_2:1

for F being Function st dom F = {{}} holds
Commute F = F