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