補題
C をアーベル圏(過去スレ019の533)とする。
f：X → Y と g：X → Z を C における射で g は単射とする。
h：X → Y＋Z を h = <f, g> (過去スレ018の872)により定義する。
Q = Coker(h) とおく。
e：Y×Z → Q を標準全射とする。
m：Y → Y＋Z を標準単射とする。

このとき、em：Y → Q は単射である。

証明
s：S → X を hs = 0 となる射とする。
hs = <f, g>s = <fs, gs> = 0
q：Y＋Z → Y を射影とする。
q<fs, gs> = gs = 0
g は単射であるから s = 0 である。
よって、h は単射である。
よって、0 → X → Y＋Z → Q → 0 は完全(過去スレ019の651)である。

u：T → Y を emu = 0 となる射とする。
上の完全列より r：T → X で mu = hr となるものがある。
mu = hr = <f, g>r = <fr, gr>
0 = qmu = q<fr, gr> = gr
g は単射だから r = 0
よって、mu = hr = 0
よって、u = 0
よって、em は単射である。
証明終