theorem Th1: :: TREES_1:1

for p, q being FinSequence holds
( p is_a_prefix_of q iff ex r being FinSequence st q = p ^ r )