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