theorem Th38: :: FINSEQ_6:38

for x being set
for f being FinSequence st f just_once_values x holds
Rev (f -| x) = (Rev f) |-- x