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

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

set FJ = Replace f,j,(f /. i);
set FI = Replace f,i,(f /. j);
A2: for k being Nat st 1 <= k & k <= len (Swap f,i,j) holds
(Swap f,i,j) . k = (Swap f,j,i) . k

proof

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

now

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

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

now

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

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

then (Swap f,i,k) . k = (Replace (Replace f,i,(f /. j)),k,(f /. i)) . k by A1, Def2
.= f /. i by A5, A6, A4, Lm2
.= (Replace (Replace f,j,(f /. i)),k,(f /. i)) . k by A5, A6, A3, Lm2
.= (Swap f,k,i) . k by A1, A8, A9, Def2 ;
hence (Swap f,i,j) . k = (Swap f,j,i) . k by A9; :: thesis: verum

end;

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

(Swap f,i,j) . k = (Replace (Replace f,i,(f /. j)),j,(f /. i)) . k by A1, Def2
.= (Replace f,k,(f /. j)) . k by A8, A10, FUNCT_7:34
.= f /. j by A5, A7, Lm2
.= (Replace (Replace f,j,(f /. i)),k,(f /. j)) . k by A5, A6, A3, Lm2 ;
hence (Swap f,i,j) . k = (Swap f,j,i) . k by A1, A8, Def2; :: thesis: verum

end;

end;

end;

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

end;

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

now

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

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

then (Swap f,i,j) . k = (Replace (Replace f,i,(f /. j)),k,(f /. i)) . k by A1, Def2
.= f /. i by A5, A6, A4, Lm2
.= (Replace f,j,(f /. i)) . k by A5, A7, A12, Lm2
.= (Replace (Replace f,j,(f /. i)),i,(f /. j)) . k by A11, FUNCT_7:34 ;
hence (Swap f,i,j) . k = (Swap f,j,i) . k by A1, Def2; :: thesis: verum

end;

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

(Swap f,i,j) . k = (Replace (Replace f,i,(f /. j)),j,(f /. i)) . k by A1, Def2
.= (Replace f,i,(f /. j)) . k by A13, FUNCT_7:34
.= f . k by A11, FUNCT_7:34
.= (Replace f,j,(f /. i)) . k by A13, FUNCT_7:34
.= (Replace (Replace f,j,(f /. i)),i,(f /. j)) . k by A11, FUNCT_7:34 ;
hence (Swap f,i,j) . k = (Swap f,j,i) . k by A1, Def2; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

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

end;

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

then Swap f,i,j = f by Def2;
hence Swap f,i,j = Swap f,j,i by A14, Def2; :: thesis: verum

end;

end;