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