let f be Function; :: thesis: for d, e, i being set holds (f +* (i,d)) +* (i,e) = f +* (i,e)
let d, e, i be set ; :: thesis: (f +* (i,d)) +* (i,e) = f +* (i,e)
A1: dom (i .--> d) = {i}
.= dom (i .--> e) ;

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

suppose A2: i in dom f ; :: thesis: (f +* (i,d)) +* (i,e) = f +* (i,e)

then i in dom (f +* (i,d)) by Th29;
hence (f +* (i,d)) +* (i,e) = (f +* (i,d)) +* (i .--> e) by Def2
.= (f +* (i .--> d)) +* (i .--> e) by A2, Def2
.= f +* ((i .--> d) +* (i .--> e)) by FUNCT_4:14
.= f +* (i .--> e) by A1, FUNCT_4:19
.= f +* (i,e) by A2, Def2 ;
:: thesis: verum

end;

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

hence (f +* (i,d)) +* (i,e) = f +* (i,e) by Def2; :: thesis: verum

end;

end;