C: dom (f +* g) c= (dom f) \/ (dom g) by Def1;
A: dom (f +* g) c= X by C, XBOOLE_1:1;
D: rng (f +* g) c= (rng f) \/ (rng g) by Th18;
rng (f +* g) c= Y by D, XBOOLE_1:1;
then f +* g is Relation of X,Y by A, RELSET_1:11;
hence f +* g is PartFunc of X,Y ; :: thesis: verum