set t = the finite binary Tree;
set T = the Function of the finite binary Tree,D;
rng the Function of the finite binary Tree,D c= D ;
then reconsider T = the Function of the finite binary Tree,D as DecoratedTree of D 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