let f, g be Function; :: thesis: ( dom f c= dom g implies f +* g = g )
assume dom f c= dom g ; :: thesis: f +* g = g
then (dom f) \/ (dom g) = dom g by XBOOLE_1:12;
then ( dom (f +* g) = dom g & ( for x being object st x in dom g holds
(f +* g) . x = g . x ) ) by Def1;
hence f +* g = g ; :: thesis: verum