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