theorem :: NEWTON04:5

for f being FinSequence
for P being Permutation of (dom f) holds P is Permutation of (dom (Rev f))