A1: dom (f +* g) c= (dom f) \/ (dom g) by Def1;
A2: dom (f +* g) c= X by A1, XBOOLE_1:1;
A3: rng (f +* g) c= (rng f) \/ (rng g) by Th17;
rng (f +* g) c= Y by A3, XBOOLE_1:1;
then f +* g is Relation of X,Y by A2, RELSET_1:4;
hence f +* g is PartFunc of X,Y ; :: thesis: verum