let A, B be set ; :: thesis: for f, g being Function st dom f = dom g & dom f c= A \/ B & f | B = g | B holds
f,g equal_outside A
let f, g be Function; :: thesis: ( dom f = dom g & dom f c= A \/ B & f | B = g | B implies f,g equal_outside A )
assume that
A1: dom f = dom g and
A2: dom f c= A \/ B ; :: thesis: ( not f | B = g | B or f,g equal_outside A )
assume f | B = g | B ; :: thesis: f,g equal_outside A
hence f | ((dom f) \ A) = g | ((dom g) \ A) by A1, A2, RELAT_1:153, XBOOLE_1:43; :: according to FUNCT_7:def 2 :: thesis: verum