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 = {} ;
then dom (f | A) = {} by RELAT_1:61;
then f | A = {} ;
hence (f +* g) | A = {} +* (g | A) by Th71
.= g | A ;
:: thesis: verum