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 A1: ( f | A = g | A & f,g equal_outside A ) ; :: thesis: f = g
thus f = f | ((dom f) \/ A) by RELAT_1:68, XBOOLE_1:7
.= f | (((dom f) \ A) \/ A) by XBOOLE_1:39
.= (f | ((dom f) \ A)) \/ (f | A) by RELAT_1:78
.= (g | ((dom g) \ A)) \/ (g | A) by A1
.= g | (((dom g) \ A) \/ A) by RELAT_1:78
.= g | ((dom g) \/ A) by XBOOLE_1:39
.= g by RELAT_1:68, XBOOLE_1:7 ; :: thesis: verum