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