let x be object ; :: according to FUNCT_1:def 14 :: thesis:
assume A1: x in dom (g +* h) ; :: thesis:
A2: dom (g +* h) = (dom g) \/ (dom h) by Def1;

per cases by A1, A2, XBOOLE_0:def 3;

suppose A3: ( x in dom g & not x in dom h ) ; :: thesis:

then g . x in f . x by FUNCT_1:def 14;
hence (g +* h) . x in f . x by A3, Th11; :: thesis:

end;

suppose A4: x in dom h ; :: thesis:

then h . x in f . x by FUNCT_1:def 14;
hence (g +* h) . x in f . x by A4, Th13; :: thesis:

end;

end;