let C be Cocartesian_category; :: thesis: for a, b, c, d, e being Object of C
for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds
[$g,k$] * (f + h) = [$(g * f),(k * h)$]
let a, b, c, d, e be Object of C; :: thesis: for f being Morphism of a,c
for h being Morphism of b,d
for g being Morphism of c,e
for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds
[$g,k$] * (f + h) = [$(g * f),(k * h)$]
let f be Morphism of a,c; :: thesis: for h being Morphism of b,d
for g being Morphism of c,e
for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds
[$g,k$] * (f + h) = [$(g * f),(k * h)$]
let h be Morphism of b,d; :: thesis: for g being Morphism of c,e
for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds
[$g,k$] * (f + h) = [$(g * f),(k * h)$]
let g be Morphism of c,e; :: thesis: for k being Morphism of d,e st Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} holds
[$g,k$] * (f + h) = [$(g * f),(k * h)$]
let k be Morphism of d,e; :: thesis: ( Hom (a,c) <> {} & Hom (b,d) <> {} & Hom (c,e) <> {} & Hom (d,e) <> {} implies [$g,k$] * (f + h) = [$(g * f),(k * h)$] )
assume that
A1: Hom (a,c) <> {} and
A2: Hom (b,d) <> {} and
A3: ( Hom (c,e) <> {} & Hom (d,e) <> {} ) ; :: thesis: [$g,k$] * (f + h) = [$(g * f),(k * h)$]
A4: Hom ((c + d),e) <> {} by A3, Th65;
A5: Hom (d,(c + d)) <> {} by Th61;
then A6: Hom (b,(c + d)) <> {} by A2, CAT_1:24;
A7: Hom (c,(c + d)) <> {} by Th61;
then A8: Hom (a,(c + d)) <> {} by A1, CAT_1:24;
[$g,k$] * (in2 (c,d)) = k by A3, Def28;
then A9: k * h = [$g,k$] * ((in2 (c,d)) * h) by A2, A4, A5, CAT_1:25;
[$g,k$] * (in1 (c,d)) = g by A3, Def28;
then g * f = [$g,k$] * ((in1 (c,d)) * f) by A1, A4, A7, CAT_1:25;
hence [$g,k$] * (f + h) = [$(g * f),(k * h)$] by A4, A8, A6, A9, Th67; :: thesis: verum