consider t being finite binary Tree;
consider T being Function of t,D;
rng T c= D ;
then reconsider T = T as DecoratedTree of by RELAT_1:def 19;
take T ; :: thesis: ( T is binary & T is finite )
thus ( dom T is binary & T is finite ) by FUNCT_2:def 1; :: according to BINTREE1:def 3 :: thesis: verum