theorem Th30: :: FINSEQ_7:30

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