let C be composable with_identities CategoryStr ; :: thesis: for f1, f2 being morphism of C st f1 |> f2 holds
( ( f1 is identity implies f1 (*) f2 = f2 ) & ( f2 is identity implies f1 (*) f2 = f1 ) )
let f1, f2 be morphism of C; :: thesis: ( f1 |> f2 implies ( ( f1 is identity implies f1 (*) f2 = f2 ) & ( f2 is identity implies f1 (*) f2 = f1 ) ) )
assume A1: f1 |> f2 ; :: thesis: ( ( f1 is identity implies f1 (*) f2 = f2 ) & ( f2 is identity implies f1 (*) f2 = f1 ) )
then A2: not C is empty by CAT_6:1;
thus ( f1 is identity implies f1 (*) f2 = f2 ) :: thesis: ( f2 is identity implies f1 (*) f2 = f1 )

proof

assume f1 is identity ; :: thesis: f1 (*) f2 = f2
then dom f1 = f1 by CAT_7:6;
then cod f2 = f1 by A1, A2, CAT_7:5;
hence f1 (*) f2 = f2 by A2, CAT_7:9; :: thesis: verum

end;

assume f2 is identity ; :: thesis: f1 (*) f2 = f1
then cod f2 = f2 by CAT_7:6;
then dom f1 = f2 by A1, A2, CAT_7:5;
hence f1 (*) f2 = f1 by A2, CAT_7:8; :: thesis: verum