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