A1: ( rng (p ^ q) = (rng p) \/ (rng q) & rng p c= D ) by RELAT_1:def 19, Th31;
rng q c= D by RELAT_1:def 19;
hence rng (p ^ q) c= D by A1, XBOOLE_1:8; :: according to FINSEQ_1:def 4 :: thesis: verum