let D be non empty set ; :: thesis: for f being FinSequence of D
for i, k, j being Nat st i <> k & j <> k 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 holds
(Swap f,i,j) . k = f . k
let i, k, j be Nat; :: thesis: ( i <> k & j <> k implies (Swap f,i,j) . k = f . k )

per cases ( ( 1 <= i & i <= len f & 1 <= j & j <= len f ) or not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ;

suppose A1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; :: thesis: ( i <> k & j <> k implies (Swap f,i,j) . k = f . k )

assume that
A2: i <> k and
A3: j <> k ; :: thesis: (Swap f,i,j) . k = f . k
(Replace (Replace f,i,(f /. j)),j,(f /. i)) . k = (Replace f,i,(f /. j)) . k by A3, FUNCT_7:34
.= f . k by A2, FUNCT_7:34 ;
hence (Swap f,i,j) . k = f . k by A1, Def2; :: thesis: verum

end;

suppose ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; :: thesis: ( i <> k & j <> k implies (Swap f,i,j) . k = f . k )

hence ( i <> k & j <> k implies (Swap f,i,j) . k = f . k ) by Def2; :: thesis: verum

end;

end;