for x being object holds
( x in Hom (a,b) iff x in { f where f is morphism of C : ( dom f = a & cod f = b ) } )

proof

let x be object ; :: thesis: ( x in Hom (a,b) iff x in { f where f is morphism of C : ( dom f = a & cod f = b ) } )

hereby :: thesis: ( x in { f where f is morphism of C : ( dom f = a & cod f = b ) } implies x in Hom (a,b) )

assume x in Hom (a,b) ; :: thesis: x in { f where f is morphism of C : ( dom f = a & cod f = b ) }
then consider f being morphism of C such that
A1: ( x = f & ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f |> f1 & f2 |> f ) ) ;
consider f1, f2 being morphism of C such that
A2: ( a = f1 & b = f2 & f |> f1 & f2 |> f ) by A1;
( dom f = a & cod f = b ) by A2, CAT_6:26, CAT_6:27, CAT_6:22;
hence x in { f where f is morphism of C : ( dom f = a & cod f = b ) } by A1; :: thesis: verum

end;

assume x in { f where f is morphism of C : ( dom f = a & cod f = b ) } ; :: thesis: x in Hom (a,b)
then consider f being morphism of C such that
A3: ( x = f & dom f = a & cod f = b ) ;
consider f1 being morphism of C such that
A4: ( dom f = f1 & f |> f1 & f1 is identity ) by CAT_6:def 18;
consider f2 being morphism of C such that
A5: ( cod f = f2 & f2 |> f & f2 is identity ) by CAT_6:def 19;
thus x in Hom (a,b) by A3, A4, A5; :: thesis: verum

end;

hence ( Hom (a,b) is Subset of (Mor C) & ( for b₁ being Subset of (Mor C) holds
( b₁ = Hom (a,b) iff b₁ = { f where f is morphism of C : ( dom f = a & cod f = b ) } ) ) ) by TARSKI:2; :: thesis: verum