正規対象ならば弱正規対象なのは明らかなので、 弱正規対象であることを仮定して正規対象でもあることを示す。

任意に 󰒚/X の対象 f:U→X をとる。 仮定から idX:X→X は 󰒚/X で推移的なので、 ある u:idX→f がとれる。

別の 󰒚/X の射 v:idX→f が存在したとする。 f は推移的なので、 ある同型射 p:idX→idX が存在して v=u∘p となるが、 そのような p は idX しかない。 したがって、 v=u である。 これにより、 idX は 󰒚/X の始対象である。

f は正規形だとして、 g が 󰒚/Y の始対象であることを示せば良い。

任意に 󰒚/Y の対象 h:V→Y をとる。 󰒚 で引き戻し X×YVVXVqpgh を計算すると、 f は 󰒚/X の始対象だから、 󰒚/X の射 u:f→p が一意に存在する。 これは、 󰒚/Y の射 q∘u:g∘f→h を定める。

他に 󰒚/Y の射 v:g∘f→h があったとする。 上の四角形の図式は引き戻しなので、 図式 WX×YVVXVvfwqphg を可換にする射 w が存在し、 これは 󰒚/X の射 w:f→p を定める。 しかし、 u の一意性により w=u である。 したがって、 v=q∘w=q∘u となり、 q∘u も一意である。 以上により、 g∘f は 󰒚/Y の始対象である。

任意に射 f:(X,x)→(X,x) をとる。 補題 3.2 によって (X,x) は正規対象でもあるから、 id(X,x) は正規形である。 さらに定理 1.9 により F は引き戻しを保つから、 El(F) は引き戻しをもつ。 したがって補題 3.3 を用いれば、 f=f∘id(X,x) も正規形であることが分かる。

さて、 SetA において余等化子 XXYfidg をとり、 y:=(Fg)x とおく。 すると、 El(F) での図式 (X,x)(X,x)(Y,y)fidg が可換になる。 これにより El(F)/(X,x) の 2 本の射 f,idX:g∘f→g が定まるが、 補題 3.3 によって g∘f は正規形なので、 f=idX となる。

以上により、 (X,x) 上の自己射は恒等射に限るので、 AutEl(F)((X,x))=1 である。

正規関手 F:SetA→Set を考える。 これは解析的なので、 定理 2.5 の議論により、 FX≅󰄘γAutNat(SetA)(γ)\(HomSetA(γ,X)×F♯γ) と書ける。 この γ は Nat(SetA) の対象全体を回る。 ここで、 F♯γ=󰄘cAutEl(F)((γ,c))\AutNat(SetA)(γ) である。 この c は (γ,c) という形の El(F) の弱正規対象の同型類の代表元全体を回る。 しかし、 今 F は正規なので、 補題 3.4 により、 F♯γ=󰄘cAutNat(SetA)(γ) となる。 ここで、 各 γ に対して、 元の対応 Aut(γ)\(Hom(γ,X)×F♯γ) ⟶ Hom(γ,X)×Aut(γ)\F♯γ [f,p@c] ⟼ (f∘p,[p@c]) [f∘p−1,p@c] ⟻ (f,[p@c]) を考えると、 これは全単射になっている。 そこで、 󰂡Fγ:=Aut(γ)\F♯γ とおけば、 定理の主張が従う。