theorem :: TREES_4:16

for x, y being object
for p being FinSequence st root-tree x = y -flat_tree p holds
( x = y & p = {} )