補題
C を>>552の条件を満たす圏とする。
e：X → Y、f：X → Y、g：X → Y、h：X → Y を C における射とする。

このとき、<[e, g], [f, h]> = [<e, f>, <g, h>]

ここで、例えば [e, g] は>>36で定義した射であり、
<e, f> は過去スレ018の872で定義した射である。

証明
p_i：Y＋Y → Y、i = 1、2 を射影とし、
μ_i：X → X＋X、i = 1、2 を入射とす。

(p_1)<[e, g], [f, h]> = [e, g]
(p_1)<[e, g], [f, h]>(μ_1) = e
(p_1)<[e, g], [f, h]>(μ_2) = g

(p_2)<[e, g], [f, h]> = [f, h]
(p_2)<[e, g], [f, h]>(μ_1) = f
(p_2)<[e, g], [f, h]>(μ_2) = h

他方、
[<e, f>, <g, h>](μ_1) = <e, f>
(p_1)[<e, f>, <g, h>](μ_1) = e
(p_2)[<e, f>, <g, h>](μ_1) = f

[<e, f>, <g, h>](μ_2) = <g, h>
(p_1)[<e, f>, <g, h>](μ_2) = g
(p_2)[<e, f>, <g, h>](μ_2) = h

よって、<[e, g], [f, h]> = [<e, f>, <g, h>]
証明終