let D be non empty set ; :: thesis: for f being FinSequence of D
for i, j being Nat holds Swap (Swap f,i,j),j,i = f
let f be FinSequence of D; :: thesis: for i, j being Nat holds Swap (Swap f,i,j),j,i = f
let i, j be Nat; :: thesis: Swap (Swap f,i,j),j,i = f

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: Swap (Swap f,i,j),j,i = f

A2: for k being Nat st 1 <= k & k <= len f holds
f . k = (Swap (Swap f,i,j),j,i) . k

proof

A3: i <= len (Swap f,i,j) by A1, Th20;
A4: j <= len (Swap f,i,j) by A1, Th20;
let k be Nat; :: thesis: ( 1 <= k & k <= len f implies f . k = (Swap (Swap f,i,j),j,i) . k )
assume that
A5: 1 <= k and
A6: k <= len f ; :: thesis: f . k = (Swap (Swap f,i,j),j,i) . k
A7: k <= len (Swap f,i,j) by A6, Th20;

now

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

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

then (Swap (Swap f,i,j),j,i) . k = (Swap f,k,j) . j by A1, A7, A4, Lm3;
hence f . k = (Swap (Swap f,i,j),j,i) . k by A1, A5, A6, Lm3; :: thesis: verum

end;

suppose A8: i <> k ; :: thesis: f . k = (Swap (Swap f,i,j),j,i) . k

now

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

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

then (Swap (Swap f,i,j),j,i) . k = (Swap f,i,k) . i by A1, A7, A3, Lm3;
hence f . k = (Swap (Swap f,i,j),j,i) . k by A1, A5, A6, Lm3; :: thesis: verum

end;

suppose A9: j <> k ; :: thesis: f . k = (Swap (Swap f,i,j),j,i) . k

set S = Swap f,i,j;
(Swap (Swap f,i,j),j,i) . k = (Replace (Replace (Swap f,i,j),j,((Swap f,i,j) /. i)),i,((Swap f,i,j) /. j)) . k by A1, A4, A3, Def2
.= (Replace (Swap f,i,j),j,((Swap f,i,j) /. i)) . k by A8, FUNCT_7:34
.= (Swap f,i,j) . k by A9, FUNCT_7:34
.= (Replace (Replace f,i,(f /. j)),j,(f /. i)) . k by A1, Def2
.= (Replace f,i,(f /. j)) . k by A9, FUNCT_7:34 ;
hence f . k = (Swap (Swap f,i,j),j,i) . k by A8, FUNCT_7:34; :: thesis: verum

end;

end;

end;

hence f . k = (Swap (Swap f,i,j),j,i) . k ; :: thesis: verum

end;

end;

end;

hence f . k = (Swap (Swap f,i,j),j,i) . k ; :: thesis: verum

end;

len (Swap (Swap f,i,j),j,i) = len (Swap f,i,j) by Th20
.= len f by Th20 ;
hence Swap (Swap f,i,j),j,i = f by A2, FINSEQ_1:18; :: thesis: verum

end;

suppose A10: ( not 1 <= i or not i <= len f or not 1 <= j or not j <= len f ) ; :: thesis: Swap (Swap f,i,j),j,i = f

then Swap (Swap f,i,j),j,i = Swap f,j,i by Def2;
hence Swap (Swap f,i,j),j,i = f by A10, Def2; :: thesis: verum

end;

end;