theorem Th35: :: TREES_3:35

for x being object
for i being Nat st i <> 0 holds
( i |-> x is FinTree-yielding iff x is finite Tree )