let A be set ; :: thesis: for f, g being A -defined Function holds f,g equal_outside A
let f, g be A -defined Function; :: thesis: f,g equal_outside A
A1: (dom g) \ A = {} by XBOOLE_1:37;
(dom f) \ A = {} by XBOOLE_1:37;
hence f | ((dom f) \ A) = {}
.= g | ((dom g) \ A) by A1 ;
:: according to FUNCT_7:def 2 :: thesis: verum