let f be Function; :: thesis: for d, r being set st d in dom f holds
dom f = dom (f +* (d .--> r))
let d, r be set ; :: thesis: ( d in dom f implies dom f = dom (f +* (d .--> r)) )
assume A1: d in dom f ; :: thesis: dom f = dom (f +* (d .--> r))
thus dom f = dom (f +* (d,r)) by Th29
.= dom (f +* (d .--> r)) by A1, Def2 ; :: thesis: verum