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 ) } )_{1} being Subset of (Mor C) holds

( b_{1} = Hom (a,b) iff b_{1} = { f where f is morphism of C : ( dom f = a & cod f = b ) } ) ) )
by TARSKI:2; :: thesis: verum

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

proof

hence
( Hom (a,b) is Subset of (Mor C) & ( for b
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 ) } )

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;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 { f where f is morphism of C : ( dom f = a & cod f = b ) }
; :: thesis: 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;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

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

( b