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

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