let F be Function; :: thesis: for x, y being set holds dom (F +* (x .--> y)) = (dom F) \/ {x}
let x, y be set ; :: thesis: dom (F +* (x .--> y)) = (dom F) \/ {x}
thus dom (F +* (x .--> y)) = (dom F) \/ (dom (x .--> y)) by FUNCT_4:def 1
.= (dom F) \/ {x} ; :: thesis: verum