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

per cases ( ( x in dom g & not x in dom h ) or x in dom h ) by A1, A2, XBOOLE_0:def 3;

suppose A3: ( x in dom g & not x in dom h ) ; :: thesis: (g +* h) . x in f . x

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

end;

suppose A4: x in dom h ; :: thesis: (g +* h) . x in f . x

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

end;

end;