theorem Th24: :: FINSEQ_6:24

for p being set
for f being FinSequence holds Rev (<*p*> ^ f) = (Rev f) ^ <*p*>