Soundness and completeness of the Birkhoff many-sorted equational calculus