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 Def7; :: thesis: verum