theorem Th5: :: AFINSQ_2:5

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