let f, g be Function; :: thesis: for A being set st f,g equal_outside A holds
g,f equal_outside A
let A be set ; :: thesis: ( f,g equal_outside A implies g,f equal_outside A )
assume f | ((dom f) \ A) = g | ((dom g) \ A) ; :: according to FUNCT_7:def 2 :: thesis: g,f equal_outside A
hence g | ((dom g) \ A) = f | ((dom f) \ A) ; :: according to FUNCT_7:def 2 :: thesis: verum