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