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: len (Swap (Swap f,i,j),j,i) = len (Swap f,i,j) by Th20
.= len f by Th20 ;
for k being Nat st 1 <= k & k <= len f holds
f . k = (Swap (Swap f,i,j),j,i) . k

proof

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

now

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

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

now

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

end;

hence f . k = (Swap (Swap f,i,j),j,i) . k ; :: 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, A4, A6, Lm3;
hence f . k = (Swap (Swap f,i,j),j,i) . k by A1, A3, 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, A5, A6, 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;

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;