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