let f, g be Function; :: thesis: for A being set st dom f misses A holds
(f +* g) | A = g | A
let A be set ; :: thesis: ( dom f misses A implies (f +* g) | A = g | A )
assume dom f misses A ; :: thesis: (f +* g) | A = g | A
then (dom f) /\ A = {} by XBOOLE_0:def 7;
then dom (f | A) = {} by RELAT_1:90;
then f | A = {} ;
hence (f +* g) | A = {} +* (g | A) by Th75
.= g | A by Th21 ;
:: thesis: verum