C: dom (f +* g) c= (dom f) \/ (dom g) by Def1;
( dom f c= X & dom g c= X ) by RELAT_1:def 18;
then (dom f) \/ (dom g) c= X \/ X by XBOOLE_1:13;
then A: dom (f +* g) c= X by C, XBOOLE_1:1;
D: rng (f +* g) c= (rng f) \/ (rng g) by Th18;
( rng f c= Y & rng g c= Y ) by RELAT_1:def 19;
then (rng f) \/ (rng g) c= Y \/ Y by XBOOLE_1:13;
then 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