let C be Category; :: thesis: for E being Subcategory of C
for f, g being Morphism of
for f', g' being Morphism of 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
for f', g' being Morphism of st f = f' & g = g' & dom g = cod f holds
g * f = g' * f'
let f, g be Morphism of ; :: thesis: for f', g' being Morphism of st f = f' & g = g' & dom g = cod f holds
g * f = g' * f'
let f', g' be Morphism of ; :: 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 A3: g' * f' = the Comp of C . g',f' 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 = g' * f' by A1, A3, A4, GRFUNC_1:8; :: thesis: verum