let C be Cocartesian_category; for a, b, c, 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, b, c, d be 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 f be 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 g be 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 h be Morphism of c,d; ( 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) <> {}
; [$(h * f),(h * g)$] = h * [$f,g$]
A3:
Hom ((a + b),c) <> {}
by A1, Th65;
A4:
Hom (b,(a + b)) <> {}
by Th61;
h * ([$f,g$] * (in2 (a,b))) = h * g
by A1, Def28;
then A5:
(h * [$f,g$]) * (in2 (a,b)) = h * g
by A2, A4, A3, CAT_1:25;
A6:
Hom (a,(a + b)) <> {}
by Th61;
A7:
( Hom (a,d) <> {} & Hom (b,d) <> {} )
by A1, A2, CAT_1:24;
h * ([$f,g$] * (in1 (a,b))) = h * f
by A1, Def28;
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, Def28; verum