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