let f be Function; :: thesis: for d, i being object holds dom (f +* (i,d)) = dom f
let x, i be object ; :: thesis: dom (f +* (i,x)) = dom f

per cases ( i in dom f or not i in dom f ) ;

suppose A1: i in dom f ; :: thesis: dom (f +* (i,x)) = dom f

then A2: {i} c= dom f by ZFMISC_1:31;
thus dom (f +* (i,x)) = dom (f +* (i .--> x)) by A1, Def2
.= (dom f) \/ (dom (i .--> x)) by FUNCT_4:def 1
.= (dom f) \/ {i}
.= dom f by A2, XBOOLE_1:12 ; :: thesis: verum

end;

suppose not i in dom f ; :: thesis: dom (f +* (i,x)) = dom f

hence dom (f +* (i,x)) = dom f by Def2; :: thesis: verum

end;

end;