let f be Function; :: thesis: for d, i being set st i in dom f holds
(f +* i,d) . i = d
let d, i be set ; :: thesis: ( i in dom f implies (f +* i,d) . i = d )
dom (i .--> d) = {i} by FUNCOP_1:19;
then A1: i in dom (i .--> d) by TARSKI:def 1;
assume i in dom f ; :: thesis: (f +* i,d) . i = d
hence (f +* i,d) . i = (f +* (i .--> d)) . i by Def3
.= (i .--> d) . i by A1, FUNCT_4:14
.= d by FUNCOP_1:87 ;
:: thesis: verum