let C be Categorial Category; 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; ( 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
; 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
; verum