let f be Function; :: thesis: for x, y being object holds dom (f +~ (x,y)) = dom f
let x, y be object ; :: thesis: dom (f +~ (x,y)) = dom f
thus dom (f +~ (x,y)) = (dom f) \/ (dom ((x .--> y) * f)) by Def1
.= dom f by RELAT_1:25, XBOOLE_1:12 ; :: thesis: verum