let D be non empty set ; :: thesis: for f being FinSequence of D
for i, j, k 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, j, k being Nat st i <> k & j <> k & 1 <= k & k <= len f holds
(Swap (f,i,j)) /. k = f /. k
let i, j, k 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:25;
k <= len (Swap (f,i,j)) by A3, Th18;
then k in dom (Swap (f,i,j)) by A2, FINSEQ_3:25;
hence (Swap (f,i,j)) /. k = (Swap (f,i,j)) . k by PARTFUN1:def 6
.= f . k by A1, Lm4
.= f /. k by A4, PARTFUN1:def 6 ;
:: thesis: verum