補題(Freyd)
C を小さいアーベル圏とし、Ab をアーベル群の圏とする。
>>414より Add(C, Ab)(>>413) はアーベル圏である。
M → E を Add(C, Ab) における本質的拡大(>>240)とする。
このとき M が単関手(>>435)であれば E も単関手である。

証明
E が単関手でないとする。
単射 m：X_0 → X で E(m) が単射でないものが存在する。
よって 0 ≠ x ∈ E(X_0) で E(m)(x) = 0 となるものがある。
x により生成される(>>439) E の部分関手を F とする。
x ∈ F(X_0) であるから F ≠ 0 である。
M → E は本質的拡大であるから>>397より M ∩ F ≠ 0 である。
よって、M(Y) ∩ F(Y) ≠ 0 となる対象 Y がある。
0 ≠ y ∈ M(Y) ∩ F(Y) とする。
F の定義より f：X_0 → Y で y = F(f)(x) となるものがある。
次の図式を押し出し(過去スレ017の867)とする。

　　　m
X_0　→　X
↓ｆ　　↓h
Y　　→　P
　　　g

アーベル圏における押し出し定理(過去スレ019の676)により g：Y → P は単射である。
0 ≠ y ∈ M(Y) かつ M は単関手であるから M(g)(y) ≠ 0 である。
M ⊂ E だから M(g)(y) = E(g)(y) ≠ 0 である。

一方、E(g)(y) = E(g)(E(f)(x)) = E(h)E(m)(x) = 0
これは矛盾である。
証明終