let x be object ; :: according to FUNCOP_1:def 6 :: thesis: ( not x in dom (f +* g) or (f +* g) . x is set )
assume x in dom (f +* g) ; :: thesis: (f +* g) . x is set
then A1: 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 A1, XBOOLE_0:def 3;

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

then (f +* g) . x = g . x by Th13;
hence (f +* g) . x is Function ; :: thesis: verum

end;

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

then (f +* g) . x = f . x by Th11;
hence (f +* g) . x is Function ; :: thesis: verum

end;

end;