theorem :: FINSEQ_7:20

for D being non empty set
for f being FinSequence of D
for i, j being Nat holds Swap ((Swap (f,i,j)),j,i) = f