theorem Th63: :: FINSEQ_5:63

for f being FinSequence
for x being object holds Rev (f ^ <*x*>) = <*x*> ^ (Rev f)