theorem Th3: :: FILEREC1:3

for p, q being FinSequence st len p = 0 holds
q = p ^ q