let f be Function; :: thesis: for n, m being set holds ((f +* (n .--> m)) +* (m .--> n)) . n = m
let n, m be set ; :: thesis: ((f +* (n .--> m)) +* (m .--> n)) . n = m
set mn = m .--> n;
set nm = n .--> m;
A1: dom (m .--> n) = {m} by FUNCOP_1:19;
then A2: m in dom (m .--> n) by TARSKI:def 1;

per cases ( n = m or n <> m ) ;

suppose A3: n = m ; :: thesis: ((f +* (n .--> m)) +* (m .--> n)) . n = m

hence ((f +* (n .--> m)) +* (m .--> n)) . n = (m .--> n) . m by A2, Th14
.= m by A3, FUNCOP_1:87 ;
:: thesis: verum

end;

suppose n <> m ; :: thesis: ((f +* (n .--> m)) +* (m .--> n)) . n = m

then A4: not n in dom (m .--> n) by A1, TARSKI:def 1;
dom (n .--> m) = {n} by FUNCOP_1:19;
then A5: n in dom (n .--> m) by TARSKI:def 1;
thus ((f +* (n .--> m)) +* (m .--> n)) . n = (f +* (n .--> m)) . n by A4, Th12
.= (n .--> m) . n by A5, Th14
.= m by FUNCOP_1:87 ; :: thesis: verum

end;

end;