let C be CategoryStr ; :: thesis: ( C is left_composable iff C opp is right_composable )

hereby :: thesis: ( C opp is right_composable implies C is left_composable )

assume A1: C is left_composable ; :: thesis: C opp is right_composable
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: ( g1 |> g2 implies ( g |> g1 (*) g2 iff g |> g1 ) )
reconsider f = g, f2 = g1, f1 = g2 as morphism of C ;
assume g1 |> g2 ; :: thesis: ( g |> g1 (*) g2 iff g |> g1 )
then A2: f1 |> f2 by FUNCT_4:42;
then A3: f1 (*) f2 = g1 (*) g2 by Th3;

hereby :: thesis: ( g |> g1 implies g |> g1 (*) g2 )

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

end;

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

end;

hence C opp is right_composable ; :: thesis: verum

end;

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

hereby :: thesis: ( f2 |> f implies f1 (*) f2 |> f )

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

end;

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

end;

hence C is left_composable ; :: thesis: verum