let C be CategoryStr ; :: thesis: ( C is right_composable iff CategoryStr(# the carrier of C, the composition of C #) is right_composable )

hereby :: thesis: ( CategoryStr(# the carrier of C, the composition of C #) is right_composable implies C is right_composable )

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

proof

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

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

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

end;

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

end;

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

end;

assume A3: CategoryStr(# the carrier of C, the composition of C #) is right_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, g1 = f1, g2 = f2 as morphism of CategoryStr(# the carrier of C, the composition of C #) ;
assume A4: f1 |> f2 ; :: thesis: ( f |> f1 (*) f2 iff f |> f1 )
then A5: g1 |> g2 ;

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

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

end;

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

end;

hence C is right_composable ; :: thesis: verum