consider t being finite Tree;
consider f being Function of t,{0 };
take f ; :: thesis: f is finite
thus f is finite ; :: thesis: verum