\(q:A\to (\sum _{y_{1},y_{2}:B}y_{1}=y_{2})\)を\(\lambda x.\mathord {\textnormal {\textsf {pair}}}(f(x),\mathord {\textnormal {\textsf {pair}}}(g(x),p(x)))\)と定義すると、\((\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(z))\circ q\equiv f\)かつ\((\lambda z.\mathord {\textnormal {\textsf {proj}}}_{1}(\mathord {\textnormal {\textsf {proj}}}_{2}(z)))\circ q\equiv g\)である。[002E]と[002J]と仮定から\(q\)が同値であると分かり、すると[002E]と[002K]から\(g\)が同値であると分かる。