:: deftheorem defines [x] CAT_4:def 19 :
for C being Cartesian_category
for a, b, c, d being Object of C
for f being Morphism of a,b
for g being Morphism of c,d holds f [x] g = <:(f * (pr1 (a,c))),(g * (pr2 (a,c))):>;