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