let f, g be Function; :: thesis: for A being set st f | A = g | A & f,g equal_outside A holds
f = g
let A be set ; :: thesis: ( f | A = g | A & f,g equal_outside A implies f = g )
assume that
A1: f | A = g | A and
A2: f,g equal_outside A ; :: thesis: f = g
thus f = f | ((dom f) \/ A) by RELAT_1:97, XBOOLE_1:7
.= f | (((dom f) \ A) \/ A) by XBOOLE_1:39
.= (f | ((dom f) \ A)) \/ (f | A) by RELAT_1:107
.= (g | ((dom g) \ A)) \/ (g | A) by A1, A2, Def2
.= g | (((dom g) \ A) \/ A) by RELAT_1:107
.= g | ((dom g) \/ A) by XBOOLE_1:39
.= g by RELAT_1:97, XBOOLE_1:7 ; :: thesis: verum