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

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

assume A1: C is with_left_identities ; :: thesis: C opp is with_right_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
( g1 |> g & g is right_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
( g1 |> g & g is right_identity ) )
assume A2: g1 in the carrier of (C opp) ; :: thesis: ex g being morphism of (C opp) st
( g1 |> g & g is right_identity )
reconsider f1 = g1 as morphism of C ;
consider f being morphism of C such that
A3: ( f |> f1 & f is left_identity ) by A1, A2;
reconsider g = f as morphism of (C opp) ;
take g ; :: thesis: ( g1 |> g & g is right_identity )
thus g1 |> g by A3, FUNCT_4:42; :: thesis: g is right_identity
for g2 being morphism of (C opp) st g2 |> g holds
g2 (*) g = g2

proof

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

end;

hence g is right_identity ; :: thesis: verum

end;

hence C opp is with_right_identities ; :: thesis: verum

end;

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

proof

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

proof

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

end;

hence f is left_identity ; :: thesis: verum

end;

hence C is with_left_identities ; :: thesis: verum