theorem :: FINSEQ_5:64

for f, g being FinSequence holds Rev (f ^ g) = (Rev g) ^ (Rev f)