let g1 be morphism of (C opp); :: thesis:
assume A2: g1 in the carrier of (C opp) ; :: thesis:
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:
thus g |> g1 by A3, FUNCT_4:42; :: thesis:
for g2 being morphism of (C opp) st g |> g2 holds
g (*) g2 = g2

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

end;

end;

end;

assume A5: C opp is with_left_identities ; :: thesis:
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 )

let f1 be morphism of C; :: thesis:
assume A6: f1 in the carrier of C ; :: thesis:
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:
thus f1 |> f by A7, FUNCT_4:42; :: thesis:
for f2 being morphism of C st f2 |> f holds
f2 (*) f = f2

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

end;

end;