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