theorem Th57: :: FINSEQ_5:57

for f being FinSequence holds
( dom f = dom (Rev f) & rng f = rng (Rev f) )