theorem :: CAT_4:77

for C being Cocartesian_category
for a, b, c being Object of C
for f being Morphism of a,c
for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds
(nabla c) * (f + g) = [$f,g$]