let f be Function; :: thesis: for i being set holds f +* (i,(f . i)) = f
let i be set ; :: thesis: f +* (i,(f . i)) = f

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

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

then A2: i .--> (f . i) = f | {i} by Th6;
thus f +* (i,(f . i)) = f +* (i .--> (f . i)) by A1, Def2
.= f by A2, FUNCT_4:75 ; :: thesis: verum

end;

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

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

end;

end;