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