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 Th18
.= len (Replace (f,j,(f /. i))) by FUNCT_7:97 ;
A4: len (Swap (f,i,j)) = len f by Th18
.= len (Replace (f,i,(f /. j))) by FUNCT_7:97 ;
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, Th18;

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

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

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

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

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

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:32 ;
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:32
.= f . k by A11, FUNCT_7:32
.= (Replace (f,j,(f /. i))) . k by A13, FUNCT_7:32
.= (Replace ((Replace (f,j,(f /. i))),i,(f /. j))) . k by A11, FUNCT_7:32 ;
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 Th18
.= len (Swap (f,j,i)) by Th18 ;
hence Swap (f,i,j) = Swap (f,j,i) by A2; :: 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;