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
x in dom (x .--> y) by TARSKI:def 1;
hence (F +* (x .--> y)) . x = (x .--> y) . x by FUNCT_4:13
.= y by FUNCOP_1:72 ;
:: thesis: verum