:: deftheorem Def23 defines [ CAT_8:def 23 :
for C1, C2 being category
for f1 being morphism of C1
for f2 being morphism of C2
for b₅ being morphism of (C1 [x] C2) holds
( ( not C1 is empty & not C2 is empty implies ( b₅ = [f1,f2] iff ( (pr1 (C1,C2)) . b₅ = f1 & (pr2 (C1,C2)) . b₅ = f2 ) ) ) & ( ( C1 is empty or C2 is empty ) implies ( b₅ = [f1,f2] iff b₅ = the morphism of (C1 [x] C2) ) ) );