let t be Element of FinTrees D; :: thesis: t is finite
dom t is finite ;
hence t is finite by FINSET_1:10; :: thesis: verum