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