let D be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 Th23
.= 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, Th13; :: thesis: verum