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

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

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

hence ((f +* (n .--> m)) +* (m .--> n)) . n = (m .--> n) . m by A1, Th13
.= m by A2, FUNCOP_1:72 ;
:: thesis: verum

end;

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

A4: n in dom (n .--> m) by TARSKI:def 1;
not n in dom (m .--> n) by A3, TARSKI:def 1;
hence ((f +* (n .--> m)) +* (m .--> n)) . n = (f +* (n .--> m)) . n by Th11
.= (n .--> m) . n by A4, Th13
.= m by FUNCOP_1:72 ;
:: thesis: verum

end;

end;