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