let D be non empty set ; for f being FinSequence of D
for i, j being Nat 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; for i, j being Nat 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 i, j be Nat; ( 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:
i in dom f
by A1, A2, FINSEQ_3:25;
set F = Replace (f,i,(f /. j));
A6:
i <= len (Replace (f,i,(f /. j)))
by A2, FUNCT_7:97;
A7:
j <= len (Replace (f,i,(f /. j)))
by A4, FUNCT_7:97;
A8:
j in dom f
by A3, A4, FINSEQ_3:25;
per cases
( i = j or i <> j )
;
suppose A9:
i = j
;
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )(Swap (f,i,j)) . i =
(Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . i
by A1, A2, A3, A4, Def2
.=
f /. i
by A1, A6, A9, Lm2
.=
f . i
by A5, PARTFUN1:def 6
;
hence
(
(Swap (f,i,j)) . i = f . j &
(Swap (f,i,j)) . j = f . i )
by A9;
verum end; suppose A10:
i <> j
;
( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )A11:
(Swap (f,i,j)) . j =
(Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . j
by A1, A2, A3, A4, Def2
.=
f /. i
by A3, A7, Lm2
;
(Swap (f,i,j)) . i =
(Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . i
by A1, A2, A3, A4, Def2
.=
(Replace (f,i,(f /. j))) . i
by A10, FUNCT_7:32
.=
f /. j
by A1, A2, Lm2
;
hence
(
(Swap (f,i,j)) . i = f . j &
(Swap (f,i,j)) . j = f . i )
by A5, A8, A11, PARTFUN1:def 6;
verum end;