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 ) )

hence f in Hom (a,b) ; :: thesis: verum

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
( dom f = a & cod f = b )
; :: thesis: 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;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

hence f in Hom (a,b) ; :: thesis: verum