theorem Th32: :: FINSEQ_7:32

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