let C be non empty non void CatStr ; :: thesis: for f being Morphism of C
for a, b being Object of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
let f be Morphism of C; :: thesis: for a, b being Object of C holds
( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
let a, b be Object of C; :: thesis: ( f in Hom (a,b) iff ( dom f = a & cod f = b ) )
thus ( f in Hom (a,b) implies ( dom f = a & cod f = b ) ) :: thesis: ( dom f = a & cod f = b implies f in Hom (a,b) )
proof
assume f in Hom (a,b) ; :: thesis: ( dom f = a & cod f = b )
then ex g being Morphism of C st
( f = g & dom g = a & cod g = b ) ;
hence ( dom f = a & cod f = b ) ; :: thesis: verum
end;
thus ( dom f = a & cod f = b implies f in Hom (a,b) ) ; :: thesis: verum