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