let C be non empty composable with_identities CategoryStr ; :: thesis: for a, b being Object of C
for f being morphism of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
let a, b be Object of C; :: thesis: for f being morphism of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
let f be morphism of C; :: thesis: ( f in Hom (a,b) iff ( dom f = a & cod f = b ) )

hereby :: thesis: ( dom f = a & cod f = b implies f in Hom (a,b) )

assume f in Hom (a,b) ; :: thesis: ( dom f = a & cod f = b )
then consider f1 being morphism of C such that
A1: ( f = f1 & a = dom f1 & b = cod f1 ) ;
thus ( dom f = a & cod f = b ) by A1; :: thesis: verum

end;

assume ( dom f = a & cod f = b ) ; :: thesis: f in Hom (a,b)
hence f in Hom (a,b) ; :: thesis: verum