let x be set ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in proj1 (f +* g) or (f +* g) . x is set )
assume x in dom (f +* g) ; :: thesis: (f +* g) . x is set
then pc: x in (dom f) \/ (dom g) by Def1;

per cases ( x in dom g or ( x in dom f & not x in dom g ) ) by pc, XBOOLE_0:def 3;

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

then (f +* g) . x = g . x by Th14;
hence (f +* g) . x is Function by S, FUNCOP_1:def 6; :: thesis: verum

end;

suppose S: ( x in dom f & not x in dom g ) ; :: thesis: (f +* g) . x is set

then (f +* g) . x = f . x by Th12;
hence (f +* g) . x is Function by S, FUNCOP_1:def 6; :: thesis: verum

end;

end;