let C be CategoryStr ; :: thesis: for f, g being morphism of C st g |> f holds
g (*) f = the composition of C . [g,f]
let f, g be morphism of C; :: thesis: ( g |> f implies g (*) f = the composition of C . [g,f] )
assume g |> f ; :: thesis: g (*) f = the composition of C . [g,f]
hence g (*) f = the composition of C . (g,f) by Def3
.= the composition of C . [g,f] by BINOP_1:def 1 ;
:: thesis: verum