let f, g be Function; :: thesis: ( dom f misses dom g implies (f +* g) \ g = f )
assume A1: dom f misses dom g ; :: thesis: (f +* g) \ g = f
then A2: f misses g by RELAT_1:179;
thus (f +* g) \ g = (f \/ g) \ g by A1, Th31
.= f by A2, XBOOLE_1:88 ; :: thesis: verum