f in Hom (a,b) by A1, Def3;
then consider f3 being morphism of C such that
A2: ( f = f3 & ex f1, f2 being morphism of C st
( a = f1 & b = f2 & f3 |> f1 & f2 |> f3 ) ) ;
consider f1, f2 being morphism of C such that
A3: ( a = f1 & b = f2 & f3 |> f1 & f2 |> f3 ) by A2;
g in Hom (b,c) by A1, Def3;
then consider g3 being morphism of C such that
A4: ( g = g3 & ex g1, g2 being morphism of C st
( b = g1 & c = g2 & g3 |> g1 & g2 |> g3 ) ) ;
consider g1, g2 being morphism of C such that
A5: ( b = g1 & c = g2 & g3 |> g1 & g2 |> g3 ) by A4;
A6: ( C is left_composable & C is right_composable ) by CAT_6:def 11;
not C is empty by A2, CAT_6:1;
then A7: g |> f by A2, A4, Th3, CAT_6:22;
( g2 |> g (*) f & g (*) f |> f1 ) by A2, A3, A4, A5, A7, A6, CAT_6:def 8, CAT_6:def 9;
then g (*) f in Hom (a,c) by A3, A5;
hence g (*) f is Morphism of a,c by Def3; :: thesis: verum