theorem :: FINSEQ_7:28

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,1,i) = ((<*(f /. i)*> ^ ((f /^ 1) | (i -' 2))) ^ <*(f /. 1)*>) ^ (f /^ i)