let C be non empty composable with_identities CategoryStr ; :: thesis: for f1, f2 being morphism of C st dom f1 = f2 holds
( f1 |> f2 & f1 (*) f2 = f1 )
let f1, f2 be morphism of C; :: thesis: ( dom f1 = f2 implies ( f1 |> f2 & f1 (*) f2 = f1 ) )
assume dom f1 = f2 ; :: thesis: ( f1 |> f2 & f1 (*) f2 = f1 )
then consider f being morphism of C such that
A1: ( f2 = f & f1 |> f & f is identity ) by CAT_6:def 18;
thus f1 |> f2 by A1; :: thesis: f1 (*) f2 = f1
thus f1 (*) f2 = f1 by A1, CAT_6:def 5, CAT_6:def 14; :: thesis: verum