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, Th5;
then A3: g9 (*) f9 = the Comp of C . (g9,f9) by A2, CAT_1:16;
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:15, CAT_1:16;
hence g (*) f = g9 (*) f9 by A1, A3, A4, GRFUNC_1:2; :: thesis: verum