let x be set ; :: according to FUNCT_1:def 20 :: thesis: ( not x in proj1 (g +* h) or (g +* h) . x in f . x )
assume Z: x in dom (g +* h) ; :: thesis: (g +* h) . x in f . x
pc: 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 Z, pc, XBOOLE_0:def 3;

suppose S: ( 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 20;
hence (g +* h) . x in f . x by S, Th12; :: thesis: verum

end;

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

then h . x in f . x by FUNCT_1:def 20;
hence (g +* h) . x in f . x by S, Th14; :: thesis: verum

end;

end;