let D be non empty set ; for f being FinSequence of D
for i, j being Nat st 1 <= i & i < j & j <= len f holds
Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
let f be FinSequence of D; for i, j being Nat st 1 <= i & i < j & j <= len f holds
Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
let i, j be Nat; ( 1 <= i & i < j & j <= len f implies Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j) )
assume that
A1:
1 <= i
and
A2:
i < j
and
A3:
j <= len f
; Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
A4:
( i <= len f & 1 <= j )
by A1, A2, A3, XXREAL_0:2;
Swap (f,i,j) =
Swap (f,j,i)
by Th21
.=
Replace ((Replace (f,j,(f /. i))),i,(f /. j))
by A1, A3, A4, Def2
;
hence
Swap (f,i,j) = ((((f | (i -' 1)) ^ <*(f /. j)*>) ^ ((f /^ i) | ((j -' i) -' 1))) ^ <*(f /. i)*>) ^ (f /^ j)
by A1, A2, A3, Th11; verum