theorem Th37: :: FINSEQ_6:37

for x being set
for f being FinSequence st f just_once_values x holds
(x .. f) + (x .. (Rev f)) = (len f) + 1