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