theorem Th31: :: TREES_2:31

for T1, T2 being DecoratedTree st dom T1 = dom T2 & ( for p being FinSequence of NAT st p in dom T1 holds
T1 . p = T2 . p ) holds
T1 = T2