For the record, the axiom of choice is not required to prove the splitting lemma. I can see why you might think it might; I once came to the same conclusion myself. To split the sequence on the right, you could start by finding a section of the surjection, invoking AC. Then you can project out the part of your section which doesn't lie in the kernel, which ensures the map is a homomorphism.
I asked about for clarification on math.SE, with a negative answer: no choice necessary. Basically, instead of starting by splitting the surjection, you recall that a retraction of the injection was part of your given data, and use it to construct the splitting of the surjection, without making any arbitrary choices.