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} by FUNCOP_1:13
.= dom (i .--> e) by FUNCOP_1:13 ;

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 Th32;
hence (f +* (i,d)) +* (i,e) = (f +* (i,d)) +* (i .--> e) by Def3
.= (f +* (i .--> d)) +* (i .--> e) by A2, Def3
.= f +* ((i .--> d) +* (i .--> e)) by FUNCT_4:14
.= f +* (i .--> e) by A1, FUNCT_4:19
.= f +* (i,e) by A2, Def3 ;
:: 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 Def3; :: thesis: verum

end;

end;