let f be Function; :: thesis: for d, i being object st i in dom f holds
(f +* (i,d)) . i = d
let d, i be object ; :: thesis: ( i in dom f implies (f +* (i,d)) . i = d )
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 Def2
.= (i .--> d) . i by A1, FUNCT_4:13
.= d by FUNCOP_1:72 ;
:: thesis: verum