theorem Th39: :: INT_5:39

for D being non empty set
for f being FinSequence of D
for i, j being Nat holds
( f is one-to-one iff Swap (f,i,j) is one-to-one )