let C be Category; :: thesis: for a, b being Object of C holds Hom (a,b) = (a Hom) /\ (Hom b)
let a, b be Object of C; :: thesis: Hom (a,b) = (a Hom) /\ (Hom b)

hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: (a Hom) /\ (Hom b) c= Hom (a,b)

let x be set ; :: thesis: ( x in Hom (a,b) implies x in (a Hom) /\ (Hom b) )
assume A1: x in Hom (a,b) ; :: thesis: x in (a Hom) /\ (Hom b)
then reconsider f = x as Morphism of C ;
A2: dom f = a by A1, CAT_1:1;
A3: cod f = b by A1, CAT_1:1;
A4: f in a Hom by A2, Th24;
f in Hom b by A3, Th23;
hence x in (a Hom) /\ (Hom b) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (a Hom) /\ (Hom b) or x in Hom (a,b) )
assume A5: x in (a Hom) /\ (Hom b) ; :: thesis: x in Hom (a,b)
then A6: x in a Hom by XBOOLE_0:def 4;
A7: x in Hom b by A5, XBOOLE_0:def 4;
reconsider f = x as Morphism of C by A5;
A8: dom f = a by A6, Th24;
cod f = b by A7, Th23;
hence x in Hom (a,b) by A8; :: thesis: verum