let C be Cocartesian_category; :: thesis: for a, c, b, d being Object of C
for f being Morphism of a,c
for g being Morphism of b,c
for h being Morphism of c,d st Hom a,c <> {} & Hom b,c <> {} & Hom c,d <> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]
let a, c, b, d be Object of C; :: thesis: for f being Morphism of a,c
for g being Morphism of b,c
for h being Morphism of c,d st Hom a,c <> {} & Hom b,c <> {} & Hom c,d <> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]
let f be Morphism of a,c; :: thesis: for g being Morphism of b,c
for h being Morphism of c,d st Hom a,c <> {} & Hom b,c <> {} & Hom c,d <> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]
let g be Morphism of b,c; :: thesis: for h being Morphism of c,d st Hom a,c <> {} & Hom b,c <> {} & Hom c,d <> {} holds
[$(h * f),(h * g)$] = h * [$f,g$]
let h be Morphism of c,d; :: thesis: ( Hom a,c <> {} & Hom b,c <> {} & Hom c,d <> {} implies [$(h * f),(h * g)$] = h * [$f,g$] )
assume that
A1: ( Hom a,c <> {} & Hom b,c <> {} ) and
A2: Hom c,d <> {} ; :: thesis: [$(h * f),(h * g)$] = h * [$f,g$]
A3: Hom (a + b),c <> {} by A1, Th70;
A4: Hom b,(a + b) <> {} by Th66;
h * ([$f,g$] * (in2 a,b)) = h * g by A1, Def29;
then A5: (h * [$f,g$]) * (in2 a,b) = h * g by A2, A4, A3, CAT_1:54;
A6: Hom a,(a + b) <> {} by Th66;
A7: ( Hom a,d <> {} & Hom b,d <> {} ) by A1, A2, CAT_1:52;
h * ([$f,g$] * (in1 a,b)) = h * f by A1, Def29;
then (h * [$f,g$]) * (in1 a,b) = h * f by A2, A6, A3, CAT_1:54;
hence [$(h * f),(h * g)$] = h * [$f,g$] by A5, A7, Def29; :: thesis: verum