for p being XFinSequence holds
( dom p = dom (Rev p) & rng p = rng (Rev p) )