A1: rng q c= D by RELAT_1:def 19;
( rng (p ^ q) = (rng p) \/ (rng q) & rng p c= D ) by Th29, RELAT_1:def 19;
then rng (p ^ q) c= D by A1, XBOOLE_1:8;
hence p ^ q is D -valued by RELAT_1:def 19; :: thesis: verum