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