let f, g be Function; :: thesis: ( dom f misses dom g implies (f +* g) | (dom f) = f )
assume dom f misses dom g ; :: thesis: (f +* g) | (dom f) = f
then A1: (dom f) \ (dom g) = dom f by XBOOLE_1:83;
dom ((f +* g) | (dom f)) = (dom (f +* g)) /\ (dom f) by RELAT_1:61
.= ((dom f) \/ (dom g)) /\ (dom f) by Def1
.= dom f by XBOOLE_1:21 ;
hence (f +* g) | (dom f) = f by A1, Th24, GRFUNC_1:3; :: thesis: verum