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

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:15
.= f +* (i .--> e) by A1, FUNCT_4:20
.= 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;