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, Def3
.= f by A2, FUNCT_4:80 ; :: thesis: verum

end;

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

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

end;

end;