theorem :: TREES_3:50

for p, q being Tree-yielding FinSequence st tree p = tree q holds
p = q