theorem :: FINSEQ_7:29

for D being non empty set
for f being FinSequence of D
for i being Nat st 1 <= i & i < len f holds
Swap (f,i,(len f)) = (((f | (i -' 1)) ^ <*(f /. (len f))*>) ^ ((f /^ i) | (((len f) -' i) -' 1))) ^ <*(f /. i)*>