let D be non empty set ; :: thesis: for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds
(Swap f,i,j) /. k = f /. k
let f be FinSequence of D; :: thesis: for i, k, j being Nat st i <> k & j <> k & 1 <= k & k <= len f holds
(Swap f,i,j) /. k = f /. k
let i, k, j be Nat; :: thesis: ( i <> k & j <> k & 1 <= k & k <= len f implies (Swap f,i,j) /. k = f /. k )
assume A1: ( i <> k & j <> k & 1 <= k & k <= len f ) ; :: thesis: (Swap f,i,j) /. k = f /. k
then k <= len (Swap f,i,j) by Th20;
then A2: k in dom (Swap f,i,j) by A1, FINSEQ_3:27;
A3: k in dom f by A1, FINSEQ_3:27;
thus (Swap f,i,j) /. k = (Swap f,i,j) . k by A2, PARTFUN1:def 8
.= f . k by A1, Lm4
.= f /. k by A3, PARTFUN1:def 8 ; :: thesis: verum