let D be non empty set ; :: thesis: for f being FinSequence of D
for p being Element of D
for i, k, j 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, k, j 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, k, j 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, k, j 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, Th7;
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, Th12
.= Replace (Replace (Replace f,k,p),i,(f /. j)),j,(f /. i) by A1, A3, A4, Th12
.= Replace (Replace (Replace f,i,(f /. j)),k,p),j,(f /. i) by A1, FUNCT_7:35
.= Replace (Replace (Replace f,i,(f /. j)),j,(f /. i)),k,p by A2, FUNCT_7:35
.= Replace (Swap f,i,j),k,p by A3, A4, A5, A6, Def2 ;
:: thesis: verum