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