consider c being morphism of C such that
A3: ( c |> f & c is left_identity ) by A2, A1, Def6;
take c ; :: thesis:
thus c |> f by A3; :: thesis:
thus c is identity by A3, Th9, A1; :: thesis:

end;

consider d being morphism of C such that
A4: ( f |> d & d is right_identity ) by A2, A1, Def7;
take d = d; :: thesis:
thus f |> d by A4; :: thesis:
thus d is identity by A4, A1, Th9; :: thesis:

end;

assume A5: for f being morphism of C st f in Mor C holds
( ex c being morphism of C st
( c |> f & c is identity ) & ex d being morphism of C st
( f |> d & d is identity ) ) ; :: thesis:
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 )

let f1 be morphism of C; :: thesis:
assume f1 in the carrier of C ; :: thesis:
then consider f being morphism of C such that
A6: ( f |> f1 & f is identity ) by A5;
take f ; :: thesis:
thus f |> f1 by A6; :: thesis:
thus f is left_identity by A6; :: thesis:

end;

let f1 be morphism of C; :: thesis:
assume f1 in the carrier of C ; :: thesis:
then consider f being morphism of C such that
A8: ( f1 |> f & f is identity ) by A5;
take f ; :: thesis:
thus f1 |> f by A8; :: thesis:
thus f is right_identity by A8; :: thesis:

end;