let f be Function; :: thesis: for d, i, j being object st i <> j holds
(f +* (i,d)) . j = f . j
let d, i, j be object ; :: thesis: ( i <> j implies (f +* (i,d)) . j = f . j )
assume A1: i <> j ; :: thesis: (f +* (i,d)) . j = f . j
A2: not j in dom (i .--> d) by A1, TARSKI:def 1;

per cases ( i in dom f or not i in dom f ) ;

suppose i in dom f ; :: thesis: (f +* (i,d)) . j = f . j

hence (f +* (i,d)) . j = (f +* (i .--> d)) . j by Def2
.= f . j by A2, FUNCT_4:11 ;
:: thesis: verum

end;

suppose not i in dom f ; :: thesis: (f +* (i,d)) . j = f . j

hence (f +* (i,d)) . j = f . j by Def2; :: thesis: verum

end;

end;