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, Th18;
A4: j <= len (Swap (f,i,j)) by A1, Th18;
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, Th18;

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

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

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