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 that
A1: 1 <= i and
A2: i <= len f and
A3: 1 <= j and
A4: j <= len f ; :: thesis: ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i )
A5: i in dom f by A1, A2, FINSEQ_3:25;
set F = Replace (f,i,(f /. j));
A6: i <= len (Replace (f,i,(f /. j))) by A2, FUNCT_7:97;
A7: j <= len (Replace (f,i,(f /. j))) by A4, FUNCT_7:97;
A8: j in dom f by A3, A4, FINSEQ_3:25;

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

suppose A9: 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, A2, A3, A4, Def2
.= f /. i by A1, A6, A9, Lm2
.= f . i by A5, PARTFUN1:def 6 ;
hence ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) by A9; :: thesis: verum

end;

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

A11: (Swap (f,i,j)) . j = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . j by A1, A2, A3, A4, Def2
.= f /. i by A3, A7, Lm2 ;
(Swap (f,i,j)) . i = (Replace ((Replace (f,i,(f /. j))),j,(f /. i))) . i by A1, A2, A3, A4, Def2
.= (Replace (f,i,(f /. j))) . i by A10, FUNCT_7:32
.= f /. j by A1, A2, Lm2 ;
hence ( (Swap (f,i,j)) . i = f . j & (Swap (f,i,j)) . j = f . i ) by A5, A8, A11, PARTFUN1:def 6; :: thesis: verum

end;

end;