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