theorem Th9: :: EUCLID_7:10

for i, j being Nat
for D being non empty set
for f being FinSequence of D 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 )