let C be Category; :: thesis: for E being Subcategory of C
for f, g being Morphism of E
for f', g' being Morphism of C st f = f' & g = g' & dom g = cod f holds
g * f = g' * f'
let E be Subcategory of C; :: thesis: for f, g being Morphism of E
for f', g' being Morphism of C st f = f' & g = g' & dom g = cod f holds
g * f = g' * f'
let f, g be Morphism of E; :: thesis: for f', g' being Morphism of C st f = f' & g = g' & dom g = cod f holds
g * f = g' * f'
let f', g' be Morphism of C; :: thesis: ( f = f' & g = g' & dom g = cod f implies g * f = g' * f' )
assume that
A1: ( f = f' & g = g' ) and
A2: dom g = cod f ; :: thesis: g * f = g' * f'
( dom g = dom g' & cod f = cod f' ) by A1, Th15;
then ( g * f = the Comp of E . g,f & [g,f] in dom the Comp of E & g' * f' = the Comp of C . g',f' & the Comp of E c= the Comp of C ) by A2, Def4, CAT_1:40, CAT_1:41;
hence g * f = g' * f' by A1, GRFUNC_1:8; :: thesis: verum