theorem :: FUNCT_4:90

for f being Function
for n, m being object holds ((f +* (n .--> m)) +* (m .--> n)) . n = m