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

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