( T . t in rng T & rng T c= D ) by FUNCT_1:def 3;
hence T . t is Element of D ; :: thesis: verum