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