theorem Th57: :: TREES_3:57

for p, q being Tree-yielding FinSequence
for T1, T2 being Tree holds tree ((p ^ <*T1*>) ^ q) = (tree ((p ^ <*T2*>) ^ q)) with-replacement (<*(len p)*>,T1)