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 FI = Replace f,i,(f /. j);
set FJ = Replace f,j,(f /. i);
A2: len (Swap f,i,j) = len f by Th20
.= len (Swap f,j,i) by Th20 ;
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

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 A3: ( 1 <= k & k <= len (Swap f,i,j) ) ; :: thesis: (Swap f,i,j) . k = (Swap f,j,i) . k
then A4: ( 1 <= k & k <= len f ) by Th20;
A5: len (Swap f,i,j) = len f by Th20
.= len (Replace f,i,(f /. j)) by Th7 ;
A6: len (Swap f,i,j) = len f by Th20
.= len (Replace f,j,(f /. i)) by Th7 ;

now

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

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

now

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

suppose A8: 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 A3, A5, Lm2
.= (Replace (Replace f,j,(f /. i)),k,(f /. i)) . k by A3, A6, Lm2
.= (Swap f,k,i) . k by A1, A7, A8, Def2 ;
hence (Swap f,i,j) . k = (Swap f,j,i) . k by A8; :: thesis: verum

end;

suppose A9: 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 A7, A9, FUNCT_7:34
.= f /. j by A4, Lm2
.= (Replace (Replace f,j,(f /. i)),k,(f /. j)) . k by A3, A6, Lm2 ;
hence (Swap f,i,j) . k = (Swap f,j,i) . k by A1, A7, Def2; :: thesis: verum

end;

end;

end;

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

end;

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

now

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

suppose A11: 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 A3, A5, Lm2
.= (Replace f,j,(f /. i)) . k by A4, A11, Lm2
.= (Replace (Replace f,j,(f /. i)),i,(f /. j)) . k by A10, FUNCT_7:34 ;
hence (Swap f,i,j) . k = (Swap f,j,i) . k by A1, Def2; :: thesis: verum

end;

suppose A12: 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 A12, FUNCT_7:34
.= f . k by A10, FUNCT_7:34
.= (Replace f,j,(f /. i)) . k by A12, FUNCT_7:34
.= (Replace (Replace f,j,(f /. i)),i,(f /. j)) . k by A10, 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;

hence Swap f,i,j = Swap f,j,i by A2, FINSEQ_1:18; :: thesis: verum

end;

suppose A13: ( 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 A13, Def2; :: thesis: verum

end;

end;