let D be non empty set ; :: thesis: for f being FinSequence of D
for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i )
let f be FinSequence of D; :: thesis: for i, j being Nat st 1 <= i & i <= len f & 1 <= j & j <= len f holds
( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i )
let i, j be Nat; :: thesis: ( 1 <= i & i <= len f & 1 <= j & j <= len f implies ( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i ) )
assume A1: ( 1 <= i & i <= len f & 1 <= j & j <= len f ) ; :: thesis: ( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i )
then A2: ( i in dom f & j in dom f ) by FINSEQ_3:27;
set F = Replace f,i,(f /. j);
A3: ( 1 <= i & i <= len (Replace f,i,(f /. j)) & 1 <= j & j <= len (Replace f,i,(f /. j)) ) by A1, Th7;

per cases ( i = j or i <> j ) ;

suppose A4: i = j ; :: thesis: ( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i )

(Swap f,i,j) . i = (Replace (Replace f,i,(f /. j)),j,(f /. i)) . i by A1, Def2
.= f /. i by A3, A4, Lm2
.= f . i by A2, PARTFUN1:def 8 ;
hence ( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i ) by A4; :: thesis: verum

end;

suppose A5: i <> j ; :: thesis: ( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i )

A6: (Swap f,i,j) . i = (Replace (Replace f,i,(f /. j)),j,(f /. i)) . i by A1, Def2
.= (Replace f,i,(f /. j)) . i by A5, FUNCT_7:34
.= f /. j by A1, Lm2 ;
(Swap f,i,j) . j = (Replace (Replace f,i,(f /. j)),j,(f /. i)) . j by A1, Def2
.= f /. i by A3, Lm2 ;
hence ( (Swap f,i,j) . i = f . j & (Swap f,i,j) . j = f . i ) by A2, A6, PARTFUN1:def 8; :: thesis: verum

end;

end;