:: deftheorem Def10 defines <: CAT_4:def 10 :
for C being Cartesian_category
for a, b, c being Object of C
for f being Morphism of c,a
for g being Morphism of c,b st Hom (c,a) <> {} & Hom (c,b) <> {} holds
for b₇ being Morphism of c,a [x] b holds
( b₇ = <:f,g:> iff ( (pr1 (a,b)) * b₇ = f & (pr2 (a,b)) * b₇ = g ) );