let C be Category; :: thesis: for E being Subcategory of C
for f being Morphism of E
for f9 being Morphism of C st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let E be Subcategory of C; :: thesis: for f being Morphism of E
for f9 being Morphism of C st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let f be Morphism of E; :: thesis: for f9 being Morphism of C st f = f9 holds
( dom f = dom f9 & cod f = cod f9 )
let f9 be Morphism of C; :: thesis: ( f = f9 implies ( dom f = dom f9 & cod f = cod f9 ) )
assume A1: f = f9 ; :: thesis: ( dom f = dom f9 & cod f = cod f9 )
set a = dom f;
set b = cod f;
reconsider a9 = dom f, b9 = cod f as Object of C by Th2;
( f in Hom ((dom f),(cod f)) & Hom ((dom f),(cod f)) c= Hom (a9,b9) ) by Def4;
hence ( dom f = dom f9 & cod f = cod f9 ) by A1, CAT_1:1; :: thesis: verum