命題
FinAb を有限アーベル群全体の圏とする。
F を>>88で定義した反変関手とする。
F は関手：FinAb → (FinAb)^o と見なせる。

このとき F は圏同値(過去スレ017の404)である。

証明
>>88より F^2 は 1_FinAb と自然同型である。
よって F は F の準逆関手(過去スレ017の394)である。
よって、過去スレ017の39より F は圏同値である。
証明終