theorem Th17: :: MATRIX_9:17

for n being Nat
for f, g being FinSequence st f ^ g in Permutations n holds
f ^ (Rev g) in Permutations n