let f be Function; :: thesis: for x, y being set holds (f +* (x .--> y)) . x = y
let x, y be set ; :: thesis: (f +* (x .--> y)) . x = y
A1: x in {x} by TARSKI:def 1;
then ( dom (x .--> y) = {x} & x in (dom f) \/ {x} ) by FUNCOP_1:19, XBOOLE_0:def 3;
hence (f +* (x .--> y)) . x = (x .--> y) . x by A1, Def1
.= y by FUNCOP_1:87 ;
:: thesis: verum