dom (g * f) c= dom f by RELAT_1:44;
then A1: dom (g * f) c= X by XBOOLE_1:1;
rng (g * f) c= Z by RELAT_1:def 19;
hence f * g is PartFunc of X,Z by A1, RELSET_1:11; :: thesis: verum