theorem Th25: :: CAT_4:25

for C being Cartesian_category
for a, b, c, d being Object of C
for f being Morphism of c,a
for g being Morphism of c,b
for h being Morphism of d,c st Hom (c,a) <> {} & Hom (c,b) <> {} & Hom (d,c) <> {} holds
<:(f * h),(g * h):> = <:f,g:> * h