let D be non empty set ; :: thesis: for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds
Swap (Swap f,i,j),j,k = Swap (Swap f,i,k),i,j
let f be FinSequence of D; :: thesis: for i, k, j being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f holds
Swap (Swap f,i,j),j,k = Swap (Swap f,i,k),i,j
let i, k, j be Nat; :: thesis: ( i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f & 1 <= k & k <= len f implies Swap (Swap f,i,j),j,k = Swap (Swap f,i,k),i,j )
assume that
A1: ( i <> k & j <> k ) and
A2: 1 <= i and
A3: i <= len f and
A4: 1 <= j and
A5: j <= len f and
A6: 1 <= k and
A7: k <= len f ; :: thesis: Swap (Swap f,i,j),j,k = Swap (Swap f,i,k),i,j
A8: ( i <= len (Replace f,i,(f /. k)) & j <= len (Replace f,i,(f /. k)) ) by A3, A5, Th7;
( j <= len (Swap f,i,j) & k <= len (Swap f,i,j) ) by A5, A7, Th20;
hence Swap (Swap f,i,j),j,k = Replace (Replace (Swap f,i,j),j,((Swap f,i,j) /. k)),k,((Swap f,i,j) /. j) by A4, A6, Def2
.= Replace (Replace (Swap f,i,j),j,((Swap f,i,j) /. k)),k,(f /. i) by A2, A3, A4, A5, Th33
.= Replace (Replace (Swap f,i,j),j,(f /. k)),k,(f /. i) by A1, A6, A7, Th32
.= Replace (Replace (Swap f,j,i),j,(f /. k)),k,(f /. i) by Th23
.= Replace (Swap (Replace f,i,(f /. k)),j,i),k,(f /. i) by A2, A3, A4, A5, Th34
.= Swap (Replace (Replace f,i,(f /. k)),k,(f /. i)),j,i by A1, A2, A4, A8, Th35
.= Swap (Swap f,i,k),j,i by A2, A3, A6, A7, Def2
.= Swap (Swap f,i,k),i,j by Th23 ;
:: thesis: verum