let D be non empty set ; :: thesis: for f being FinSequence of D
for i, j, k 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, j, k 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, j, k 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, FUNCT_7:97;
( j <= len (Swap (f,i,j)) & k <= len (Swap (f,i,j)) ) by A5, A7, Th18;
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, Th31
.= Replace ((Replace ((Swap (f,i,j)),j,(f /. k))),k,(f /. i)) by A1, A6, A7, Th30
.= Replace ((Replace ((Swap (f,j,i)),j,(f /. k))),k,(f /. i)) by Th21
.= Replace ((Swap ((Replace (f,i,(f /. k))),j,i)),k,(f /. i)) by A2, A3, A4, A5, Th32
.= Swap ((Replace ((Replace (f,i,(f /. k))),k,(f /. i))),j,i) by A1, A2, A4, A8, Th33
.= Swap ((Swap (f,i,k)),j,i) by A2, A3, A6, A7, Def2
.= Swap ((Swap (f,i,k)),i,j) by Th21 ;
:: thesis: verum