let C be CategoryStr ; :: thesis:

hereby :: thesis:

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

proof

let g, g1, g2 be morphism of (C opp); :: thesis:
reconsider f = g, f2 = g1, f1 = g2 as morphism of C ;
assume g1 |> g2 ; :: thesis:
then A2: f1 |> f2 by FUNCT_4:42;
then A3: f1 (*) f2 = g1 (*) g2 by Th3;

hereby :: thesis:

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

end;

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

end;

hence C opp is right_composable ; :: thesis:

end;

assume A4: C opp is right_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, g2 = f1, g1 = f2 as morphism of (C opp) ;
assume A5: f1 |> f2 ; :: thesis:
then A6: g1 |> g2 by FUNCT_4:42;
A7: f1 (*) f2 = g1 (*) g2 by A5, Th3;

hereby :: thesis:

assume f1 (*) f2 |> f ; :: thesis:
then g |> g1 (*) g2 by A7, FUNCT_4:42;
then g |> g1 by A4, A6;
hence f2 |> f by FUNCT_4:42; :: thesis:

end;

assume f2 |> f ; :: thesis:
then g |> g1 by FUNCT_4:42;
then g |> g1 (*) g2 by A4, A6;
hence f1 (*) f2 |> f by A7, FUNCT_4:42; :: thesis:

end;

hence C is left_composable ; :: thesis: