I'm not an expert on formal verification, so I'll share a non-expert perspective.
A general approach is: formalize the semantics of each operation (in whatever logic is accepted by your chosen theorem prover), then formulate the theorem you are trying to prove (that both queries yield the same results for all possible databases), then ask the theorem prover to prove it.
The details of how you go about that will depend a lot on the particular theorem prover you have chosen, the set of operations you want to support, how you formalize the semantics of each operation mathematically, and how much human assistance you want to provide the theorem prover.
There are a wide range of theorem provers, which strike different points in the tradeoff between automated proving (without human assistance) vs expressivity and based on different mathematical logics.
There are also likely to be multiple ways to formulate the semantics of the operations mathematically. For instance, suppose you know that all of your operations will only select some of the rows of input and/or re-order them, but will not produce new rows not found in the input or modify existing rows. Then the output of an operation could be represented by a sequence $(r_1,r_2,\dots,r_k)$ of indices, where $r_i$ is the index of a row in the input (namely, the $i$th row returned by the operation). Then each operation becomes a function $f$ that maps from an input to a sequence $r$; you can formulate the semantics of the composition of operations; and proving the equivalence of operations amounts to proving that they represent the same function.
Another approach, instead of formulating this as theorem proving of mathematical statements, would be to formulate this as formal verification of programs. You can view an operation as a program that takes an array as input (the database is an array of rows), and produces an array as output (an array of rows). You can write down code that implements the sort operation, and code that implements the match operation. So, now you can write down two subroutines: one that sorts then matches; and one that matches then sorts. Finally, you can try to use formal verification to prove that both subroutines yield the same output, on all possible inputs.
If you try to do this in practice, you'll probably quickly run into the limitations of the current state of the art in automated theorem proving and program verification. Theorem provers generally require a lot of hand-holding to prove non-trivial mathematical statements (they may require you to specify statements of lemmas that are useful to proof, or give hints on how to prove a statement). Program verification tools also generally require a lot of hand-holding to verify non-trivial programs correct (for instance, they may require you to specify many loop invariants). They are getting better, but it's still a non-trivial effort.
To learn more, you might start by looking at how to formally verify a sorting algorithm correct. That will give you ideas on possible ways you could formulate the kinds of properties you want to prove.
See also A general picture of formal verification in software.