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 ))] )
assume A1: dom g = cod f ; :: thesis: g * f = [[(dom f),(cod g)],((g `2 ) * (f `2 ))]
A2: ( g `11 = dom g & g `12 = cod g & f `11 = dom f & f `12 = cod f ) by CAT_5:13;
then consider gg being Functor of g `11 ,g `12 such that
A3: g = [[(dom g),(cod g)],gg] by CAT_5:def 6;
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;
thus g * f = [[(dom f),(cod g)],(gg * ff)] by A1, A2, A3, A4, CAT_5:def 6
.= [[(dom f),(cod g)],(gg * (f `2 ))] by A4, MCART_1:7
.= [[(dom f),(cod g)],((g `2 ) * (f `2 ))] by A3, MCART_1:7 ; :: thesis: verum