let D be non empty set ; for f being FinSequence of D
for p being Element of D
for i, j, k being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds
Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
let f be FinSequence of D; for p being Element of D
for i, j, k being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds
Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
let p be Element of D; for i, j, k being Nat st i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f holds
Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
let i, j, k be Nat; ( i <> k & j <> k & 1 <= i & i <= len f & 1 <= j & j <= len f implies Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p) )
assume that
A1:
i <> k
and
A2:
j <> k
and
A3:
1 <= i
and
A4:
i <= len f
and
A5:
1 <= j
and
A6:
j <= len f
; Swap ((Replace (f,k,p)),i,j) = Replace ((Swap (f,i,j)),k,p)
( i <= len (Replace (f,k,p)) & j <= len (Replace (f,k,p)) )
by A4, A6, FUNCT_7:97;
hence Swap ((Replace (f,k,p)),i,j) =
Replace ((Replace ((Replace (f,k,p)),i,((Replace (f,k,p)) /. j))),j,((Replace (f,k,p)) /. i))
by A3, A5, Def2
.=
Replace ((Replace ((Replace (f,k,p)),i,(f /. j))),j,((Replace (f,k,p)) /. i))
by A2, A5, A6, Th10
.=
Replace ((Replace ((Replace (f,k,p)),i,(f /. j))),j,(f /. i))
by A1, A3, A4, Th10
.=
Replace ((Replace ((Replace (f,i,(f /. j))),k,p)),j,(f /. i))
by A1, FUNCT_7:33
.=
Replace ((Replace ((Replace (f,i,(f /. j))),j,(f /. i))),k,p)
by A2, FUNCT_7:33
.=
Replace ((Swap (f,i,j)),k,p)
by A3, A4, A5, A6, Def2
;
verum