let C be CategoryStr ; :: thesis:

hereby :: thesis:

assume A1: C is with_right_identities ; :: thesis:
for g1 being morphism of CategoryStr(# the carrier of C, the composition of C #) st g1 in the carrier of CategoryStr(# the carrier of C, the composition of C #) holds
ex g being morphism of CategoryStr(# the carrier of C, the composition of C #) st
( g1 |> g & g is right_identity )

proof

let g1 be morphism of CategoryStr(# the carrier of C, the composition of C #); :: thesis:
reconsider f1 = g1 as morphism of C ;
assume g1 in the carrier of CategoryStr(# the carrier of C, the composition of C #) ; :: thesis:
then consider f being morphism of C such that
A2: ( f1 |> f & f is right_identity ) by A1;
reconsider g = f as morphism of CategoryStr(# the carrier of C, the composition of C #) ;
take g ; :: thesis:
thus g1 |> g by A2; :: thesis:
thus g is right_identity by A2, Th18; :: thesis:

end;

hence CategoryStr(# the carrier of C, the composition of C #) is with_right_identities ; :: thesis:

end;

assume A3: CategoryStr(# the carrier of C, the composition of C #) is with_right_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 )

proof

let f1 be morphism of C; :: thesis:
reconsider g1 = f1 as morphism of CategoryStr(# the carrier of C, the composition of C #) ;
assume f1 in the carrier of C ; :: thesis:
then consider g being morphism of CategoryStr(# the carrier of C, the composition of C #) such that
A4: ( g1 |> g & g is right_identity ) by A3;
reconsider f = g as morphism of C ;
take f ; :: thesis:
thus f1 |> f by A4; :: thesis:
thus f is right_identity by A4, Th18; :: thesis:

end;

hence C is with_right_identities ; :: thesis: