MATH.19:5.1 - Choose the intermediate equality that proves injectivity
Let f:A->B and g:B->A satisfy g(f(a))=a for every a in A. Prove that f is injective.
Work backward from injectivity: choose arbitrary a,b in A and assume f(a)=f(b). The required conclusion is a=b. The given identity involves g(f(a)), so work forward by applying g to the assumed equality:
g(f(a))=g(f(b)).
Substitute the two given identities to obtain a=b. The intermediate equality connects the assumption to the goal; no larger theory is needed.
Now replace the given identity by f(g(b))=b for every b in B. The same proof cannot simplify g(f(a)). What it does supply is surjectivity of f: for an arbitrary b, choose a=g(b), then f(a)=b.
For a concrete separating case, take A={0,1}, B={*}, f(0)=f(1)=*, and g(*)=0. The changed identity holds, but f is not injective. The failure identifies which composite was required and produces the useful conclusion that remains. MATH.18 can use these two composites when comparing descriptions.