let C be CategoryStr ; :: thesis:

hereby :: thesis:

assume A1: C is left_composable ; :: thesis:
for g, g1, g2 being morphism of CategoryStr(# the carrier of C, the composition of C #) st g1 |> g2 holds
( g1 (*) g2 |> g iff g2 |> g )

proof

let g, g1, g2 be morphism of CategoryStr(# the carrier of C, the composition of C #); :: thesis:
reconsider f = g, f1 = g1, f2 = g2 as morphism of C ;
assume g1 |> g2 ; :: thesis:
then A2: f1 |> f2 ;

hereby :: thesis:

assume g1 (*) g2 |> g ; :: thesis:
then f1 (*) f2 |> f by A2, Th11;
then f2 |> f by A2, A1;
hence g2 |> g ; :: thesis:

end;

assume g2 |> g ; :: thesis:
then f2 |> f ;
then f1 (*) f2 |> f by A2, A1;
hence g1 (*) g2 |> g by A2, Th11; :: thesis:

end;

hence CategoryStr(# the carrier of C, the composition of C #) is left_composable ; :: thesis:

end;

assume A3: CategoryStr(# the carrier of C, the composition of C #) is left_composable ; :: thesis:
for f, f1, f2 being morphism of C st f1 |> f2 holds
( f1 (*) f2 |> f iff f2 |> f )

proof

let f, f1, f2 be morphism of C; :: thesis:
reconsider g = f, g1 = f1, g2 = f2 as morphism of CategoryStr(# the carrier of C, the composition of C #) ;
assume A4: f1 |> f2 ; :: thesis:
then A5: g1 |> g2 ;

hereby :: thesis:

assume f1 (*) f2 |> f ; :: thesis:
then g1 (*) g2 |> g by A4, Th11;
then g2 |> g by A3, A5;
hence f2 |> f ; :: thesis:

end;

assume f2 |> f ; :: thesis:
then g2 |> g ;
then g1 (*) g2 |> g by A3, A5;
hence f1 (*) f2 |> f by A4, Th11; :: thesis:

end;

hence C is left_composable ; :: thesis: