let i, j be Nat; for D being non empty set
for f being FinSequence of D st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
let D be non empty set ; for f being FinSequence of D st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
let f be FinSequence of D; ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) )
assume that
A1:
1 <= i
and
A2:
i <= len f
and
A3:
1 <= j
and
A4:
j <= len f
; ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
A5:
len (Replace (f,i,(f /. j))) = len f
by FINSEQ_7:5;
A6:
len (Swap (f,i,j)) = len f
by FINSEQ_7:18;
then
(Swap (f,i,j)) /. j = (Swap (f,i,j)) . j
by A3, A4, FINSEQ_4:15;
then A7: (Swap (f,i,j)) . j =
(Replace ((Replace (f,i,(f /. j))),j,(f /. i))) /. j
by A1, A2, A3, A4, FINSEQ_7:def 2
.=
f /. i
by A3, A4, A5, FINSEQ_7:8
.=
f . i
by A1, A2, FINSEQ_4:15
;
A8:
Swap (f,i,j) = Swap (f,j,i)
by FINSEQ_7:21;
A9:
len (Replace (f,j,(f /. i))) = len f
by FINSEQ_7:5;
(Swap (f,i,j)) /. i = (Swap (f,i,j)) . i
by A1, A2, A6, FINSEQ_4:15;
then (Swap (f,i,j)) . i =
(Replace ((Replace (f,j,(f /. i))),i,(f /. j))) /. i
by A1, A2, A3, A4, A8, FINSEQ_7:def 2
.=
f /. j
by A1, A2, A9, FINSEQ_7:8
.=
f . j
by A3, A4, FINSEQ_4:15
;
hence
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
by A7; verum