let f be Function; :: thesis: for a, b, A being set st a in A holds
f,f +* (a,b) equal_outside A
let a, b, A be set ; :: thesis: ( a in A implies f,f +* (a,b) equal_outside A )

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

suppose A1: a in dom f ; :: thesis: ( a in A implies f,f +* (a,b) equal_outside A )

assume a in A ; :: thesis: f,f +* (a,b) equal_outside A
then {a} c= A by ZFMISC_1:31;
then A2: dom (a .--> b) c= A ;
f +* (a,b) = f +* (a .--> b) by A1, Def2;
hence f,f +* (a,b) equal_outside A by A2, Th28; :: thesis: verum

end;

suppose not a in dom f ; :: thesis: ( a in A implies f,f +* (a,b) equal_outside A )

then f +* (a,b) = f by Def2;
hence ( a in A implies f,f +* (a,b) equal_outside A ) ; :: thesis: verum

end;

end;