let C be Cocartesian_category; :: thesis: for a, c, b 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$]
let a, c, b be Object of C; :: thesis: 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$]
let f be Morphism of a,c; :: thesis: for g being Morphism of b,c st Hom (a,c) <> {} & Hom (b,c) <> {} holds
(nabla c) * (f + g) = [$f,g$]
let g be Morphism of b,c; :: thesis: ( Hom (a,c) <> {} & Hom (b,c) <> {} implies (nabla c) * (f + g) = [$f,g$] )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,c) <> {} ; :: thesis: (nabla c) * (f + g) = [$f,g$]
Hom (c,c) <> {} by CAT_1:27;
hence (nabla c) * (f + g) = [$((id c) * f),((id c) * g)$] by A1, A2, Th80
.= [$f,((id c) * g)$] by A1, CAT_1:28
.= [$f,g$] by A2, CAT_1:28 ;
:: thesis: verum