let F be Function; :: thesis: for x, y being set holds x in dom (F +* (x .--> y))
let x, y be set ; :: thesis: x in dom (F +* (x .--> y))
dom (x .--> y) = {x} by FUNCOP_1:19;
then A1: x in dom (x .--> y) by TARSKI:def 1;
dom (x .--> y) c= dom (F +* (x .--> y)) by FUNCT_4:11;
hence x in dom (F +* (x .--> y)) by A1; :: thesis: verum