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:27;
set F = Replace f,i,(f /. j);
A6: i <= len (Replace f,i,(f /. j)) by A2, FUNCT_7:99;
A7: j <= len (Replace f,i,(f /. j)) by A4, FUNCT_7:99;
A8: j in dom f by A3, A4, FINSEQ_3:27;

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 8 ;
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:34
.= 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 8; :: thesis: verum

end;

end;