let C be non empty non void CatStr ; :: thesis: for f being Morphism of C holds f is Morphism of dom f, cod f
let f be Morphism of C; :: thesis: f is Morphism of dom f, cod f
f in Hom ((dom f),(cod f)) ;
hence f is Morphism of dom f, cod f by Def3; :: thesis: verum