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

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

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

proof

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

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

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

end;

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

end;

hence C opp is left_composable ; :: thesis: verum

end;

assume A4: C opp is left_composable ; :: thesis: C is right_composable
for f, f1, f2 being morphism of C st f1 |> f2 holds
( f |> f1 (*) f2 iff f |> f1 )

proof

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

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

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

end;

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

end;

hence C is right_composable ; :: thesis: verum