let C be CategoryStr ; :: thesis: ( C is with_right_identities iff C opp is with_left_identities )

hereby :: thesis: ( C opp is with_left_identities implies C is with_right_identities )

assume A1: C is with_right_identities ; :: thesis: C opp is with_left_identities
for g1 being morphism of (C opp) st g1 in the carrier of (C opp) holds
ex g being morphism of (C opp) st
( g |> g1 & g is left_identity )

proof

let g1 be morphism of (C opp); :: thesis: ( g1 in the carrier of (C opp) implies ex g being morphism of (C opp) st
( g |> g1 & g is left_identity ) )
assume A2: g1 in the carrier of (C opp) ; :: thesis: ex g being morphism of (C opp) st
( g |> g1 & g is left_identity )
reconsider f1 = g1 as morphism of C ;
consider f being morphism of C such that
A3: ( f1 |> f & f is right_identity ) by A1, A2;
reconsider g = f as morphism of (C opp) ;
take g ; :: thesis: ( g |> g1 & g is left_identity )
thus g |> g1 by A3, FUNCT_4:42; :: thesis: g is left_identity
for g2 being morphism of (C opp) st g |> g2 holds
g (*) g2 = g2

proof

let g2 be morphism of (C opp); :: thesis: ( g |> g2 implies g (*) g2 = g2 )
reconsider f2 = g2 as morphism of C ;
assume g |> g2 ; :: thesis: g (*) g2 = g2
then A4: f2 |> f by FUNCT_4:42;
then f2 (*) f = f2 by A3;
hence g (*) g2 = g2 by A4, Th3; :: thesis: verum

end;

hence g is left_identity ; :: thesis: verum

end;

hence C opp is with_left_identities ; :: thesis: verum

end;

assume A5: C opp is with_left_identities ; :: thesis: C is with_right_identities
for f1 being morphism of C st f1 in the carrier of C holds
ex f being morphism of C st
( f1 |> f & f is right_identity )

proof

let f1 be morphism of C; :: thesis: ( f1 in the carrier of C implies ex f being morphism of C st
( f1 |> f & f is right_identity ) )
assume A6: f1 in the carrier of C ; :: thesis: ex f being morphism of C st
( f1 |> f & f is right_identity )
reconsider g1 = f1 as morphism of (C opp) ;
consider g being morphism of (C opp) such that
A7: ( g |> g1 & g is left_identity ) by A5, A6;
reconsider f = g as morphism of C ;
take f ; :: thesis: ( f1 |> f & f is right_identity )
thus f1 |> f by A7, FUNCT_4:42; :: thesis: f is right_identity
for f2 being morphism of C st f2 |> f holds
f2 (*) f = f2

proof

let f2 be morphism of C; :: thesis: ( f2 |> f implies f2 (*) f = f2 )
reconsider g2 = f2 as morphism of (C opp) ;
assume A8: f2 |> f ; :: thesis: f2 (*) f = f2
then g |> g2 by FUNCT_4:42;
then g (*) g2 = g2 by A7;
hence f2 (*) f = f2 by A8, Th3; :: thesis: verum

end;

hence f is right_identity ; :: thesis: verum

end;

hence C is with_right_identities ; :: thesis: verum