let D be non empty set ; 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; 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; ( 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
; 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)
; verum