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:25;
A6: Hom (a,(a + b)) <> {} by Th66;
A7: ( Hom (a,d) <> {} & Hom (b,d) <> {} ) by A1, A2, CAT_1:24;
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:25;
hence [$(h * f),(h * g)$] = h * [$f,g$] by A5, A7, Def29; :: thesis: verum