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

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

assume A1: C is left_composable ; :: thesis: CategoryStr(# the carrier of C, the composition of C #) is left_composable
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: ( g1 |> g2 implies ( g1 (*) g2 |> g iff g2 |> g ) )
reconsider f = g, f1 = g1, f2 = g2 as morphism of C ;
assume g1 |> g2 ; :: thesis: ( g1 (*) g2 |> g iff g2 |> g )
then A2: f1 |> f2 ;

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

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

end;

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

end;

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

end;

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

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

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

end;

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

end;

hence C is left_composable ; :: thesis: verum