let f be Function; :: thesis: for a, b being object holds (f +* (a .--> b)) . a = b
let a, b be object ; :: thesis: (f +* (a .--> b)) . a = b
a in dom (a .--> b) by TARSKI:def 1;
hence (f +* (a .--> b)) . a = (a .--> b) . a by FUNCT_4:13
.= b by FUNCOP_1:72 ;
:: thesis: verum