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 A1: ( 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 ) ; :: thesis: Swap (Swap f,i,j),k,l = Swap (Swap f,k,l),i,j
set F = Swap f,i,j;
A2: ( i <= len (Swap f,i,j) & j <= len (Swap f,i,j) & k <= len (Swap f,i,j) & l <= len (Swap f,i,j) ) by A1, Th20;
A3: ( i <= len (Replace f,k,(f /. l)) & j <= len (Replace f,k,(f /. l)) & k <= len (Replace f,k,(f /. l)) & l <= len (Replace f,k,(f /. l)) ) by A1, Th7;
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 A1, A2, Def2
.= Replace (Replace (Swap f,i,j),k,((Swap f,i,j) /. l)),l,(f /. k) by A1, Th32
.= Replace (Replace (Swap f,i,j),k,(f /. l)),l,(f /. k) by A1, 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, Th35
.= Swap (Replace (Replace f,k,(f /. l)),l,(f /. k)),j,i by A1, A3, Th35
.= Swap (Swap f,k,l),j,i by A1, 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