過去スレ017の820の双対

命題
C を圏とする。
C において始対象(過去スレ017の288)と任意のファイバー積(過去スレ017の866)が存在すれば
C において任意の有限個の対象の余積(過去スレ017の837)と
任意の差余核(過去スレ017の850)が存在する。

証明
s を C の始対象とする。
X と Y を C の対象とする。
ファイバー余積 (X＋Y)_s は余積 X＋Y と同型である。
よって、過去スレ017の848より、C の任意の有限個の対象の余積が存在する。
>>3より、任意の差余核が存在する。
証明終