theorem Th31: :: FINSEQ_7:31

for D being non empty set
for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) /. i = f /. j & (Swap (f,i,j)) /. j = f /. i )