( rng (T | p) c= rng T & rng T c= D ) by Th34, RELAT_1:def 19;
then rng (T | p) c= D by XBOOLE_1:1;
hence T | p is D -valued by RELAT_1:def 19; :: thesis: verum