let C be Categorial Category; :: thesis: for f, g being Morphism of C st dom g = cod f holds
g (*) f = [[(dom f),(cod g)],((g `2) * (f `2))]
let f, g be Morphism of C; :: thesis: ( dom g = cod f implies g (*) f = [[(dom f),(cod g)],((g `2) * (f `2))] )
A1: g `11 = dom g by CAT_5:13;
A2: f `11 = dom f by CAT_5:13;
assume A3: dom g = cod f ; :: thesis: g (*) f = [[(dom f),(cod g)],((g `2) * (f `2))]
then consider ff being Functor of f `11 ,g `11 such that
A4: f = [[(dom f),(cod f)],ff] by A1, A2, CAT_5:def 6;
A5: g `12 = cod g by CAT_5:13;
then consider gg being Functor of g `11 ,g `12 such that
A6: g = [[(dom g),(cod g)],gg] by A1, CAT_5:def 6;
thus g (*) f = [[(dom f),(cod g)],(gg * ff)] by A3, A1, A5, A2, A6, A4, CAT_5:def 6
.= [[(dom f),(cod g)],(gg * (f `2))] by A4
.= [[(dom f),(cod g)],((g `2) * (f `2))] by A6 ; :: thesis: verum