let C be CategoryStr ; :: thesis: for f being morphism of C st C is with_identities holds
( f is left_identity iff f is right_identity )
let f be morphism of C; :: thesis: ( C is with_identities implies ( f is left_identity iff f is right_identity ) )
assume A1: C is with_identities ; :: thesis: ( f is left_identity iff f is right_identity )

hereby :: thesis: ( f is right_identity implies f is left_identity )

assume A2: f is left_identity ; :: thesis: f is right_identity
for f1 being morphism of C st f1 |> f holds
f1 (*) f = f1

proof

let f1 be morphism of C; :: thesis: ( f1 |> f implies f1 (*) f = f1 )
assume A3: f1 |> f ; :: thesis: f1 (*) f = f1
then not C is empty ;
then consider g being morphism of C such that
A4: ( f |> g & g is right_identity ) by A1, Def7;
f = f (*) g by A4
.= g by A2, A4 ;
hence f1 (*) f = f1 by A4, A3; :: thesis: verum

end;

hence f is right_identity ; :: thesis: verum

end;

assume A5: f is right_identity ; :: thesis: f is left_identity
for f1 being morphism of C st f |> f1 holds
f (*) f1 = f1

proof

let f1 be morphism of C; :: thesis: ( f |> f1 implies f (*) f1 = f1 )
assume A6: f |> f1 ; :: thesis: f (*) f1 = f1
then not C is empty ;
then consider g being morphism of C such that
A7: ( g |> f & g is left_identity ) by A1, Def6;
f = g (*) f by A7
.= g by A5, A7 ;
hence f (*) f1 = f1 by A7, A6; :: thesis: verum

end;

hence f is left_identity ; :: thesis: verum