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

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