let f be Function; :: thesis: for a, b, n, m being set holds ((f +* (a .--> b)) +* (m .--> n)) . m = n
let a, b, n, m be set ; :: thesis: ((f +* (a .--> b)) +* (m .--> n)) . m = n
set mn = m .--> n;
dom (m .--> n) = {m} by FUNCOP_1:13;
then m in dom (m .--> n) by TARSKI:def 1;
hence ((f +* (a .--> b)) +* (m .--> n)) . m = (m .--> n) . m by Th14
.= n by FUNCOP_1:72 ;
:: thesis: verum