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 that
A1: ( i <> k & j <> k ) and
A2: 1 <= k and
A3: k <= len f ; :: thesis: (Swap f,i,j) /. k = f /. k
A4: k in dom f by A2, A3, FINSEQ_3:27;
k <= len (Swap f,i,j) by A3, Th20;
then k in dom (Swap f,i,j) by A2, FINSEQ_3:27;
hence (Swap f,i,j) /. k = (Swap f,i,j) . k by PARTFUN1:def 8
.= f . k by A1, Lm4
.= f /. k by A4, PARTFUN1:def 8 ;
:: thesis: verum