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