let A be Category; for a, b, c, d being Object of A st Hom (a,b) meets Hom (c,d) holds
( a = c & b = d )
let a, b, c, d be Object of A; ( Hom (a,b) meets Hom (c,d) implies ( a = c & b = d ) )
assume
Hom (a,b) meets Hom (c,d)
; ( a = c & b = d )
then consider x being object such that
A1:
x in Hom (a,b)
and
A2:
x in Hom (c,d)
by XBOOLE_0:3;
reconsider x = x as Morphism of A by A1;
A3:
cod x = b
by A1, CAT_1:1;
dom x = a
by A1, CAT_1:1;
hence
( a = c & b = d )
by A2, A3, CAT_1:1; verum