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

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