let C be Cocartesian_category; :: thesis: for a, c, b, 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, c, b, 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, Th70;
A5: Hom d,(c + d) <> {} by Th66;
then A6: Hom b,(c + d) <> {} by A2, CAT_1:52;
A7: Hom c,(c + d) <> {} by Th66;
then A8: Hom a,(c + d) <> {} by A1, CAT_1:52;
[$g,k$] * (in2 c,d) = k by A3, Def29;
then A9: k * h = [$g,k$] * ((in2 c,d) * h) by A2, A4, A5, CAT_1:54;
[$g,k$] * (in1 c,d) = g by A3, Def29;
then g * f = [$g,k$] * ((in1 c,d) * f) by A1, A4, A7, CAT_1:54;
hence [$g,k$] * (f + h) = [$(g * f),(k * h)$] by A4, A8, A6, A9, Th72; :: thesis: verum