theorem Th33: :: TREES_9:33

for D being non empty set
for r being FinSequence of D
for r1, r2 being FinSequence
for k being Nat st k + 1 <= len r & r1 = r | (Seg (k + 1)) & r2 = r | (Seg k) holds
ex x being Element of D st r1 = r2 ^ <*x*>