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:56;
hence (nabla c) * (f + g) = [$((id c) * f),((id c) * g)$] by A1, A2, Th80
.= [$f,((id c) * g)$] by A1, CAT_1:57
.= [$f,g$] by A2, CAT_1:57 ;
:: thesis: verum