let C be CategoryStr ; :: thesis: ( C is with_right_identities iff CategoryStr(# the carrier of C, the composition of C #) is with_right_identities )

hereby :: thesis: ( CategoryStr(# the carrier of C, the composition of C #) is with_right_identities implies C is with_right_identities )

assume A1: C is with_right_identities ; :: thesis: CategoryStr(# the carrier of C, the composition of C #) is with_right_identities
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: ( g1 in the carrier of CategoryStr(# the carrier of C, the composition of C #) implies ex g being morphism of CategoryStr(# the carrier of C, the composition of C #) st
( g1 |> g & g is right_identity ) )
reconsider f1 = g1 as morphism of C ;
assume g1 in the carrier of CategoryStr(# the carrier of C, the composition of C #) ; :: thesis: ex g being morphism of CategoryStr(# the carrier of C, the composition of C #) st
( g1 |> g & g is right_identity )
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: ( g1 |> g & g is right_identity )
thus g1 |> g by A2; :: thesis: g is right_identity
thus g is right_identity by A2, Th18; :: thesis: verum

end;

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

end;

assume A3: CategoryStr(# the carrier of C, the composition of C #) is with_right_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 ) )
reconsider g1 = f1 as morphism of CategoryStr(# the carrier of C, the composition of C #) ;
assume f1 in the carrier of C ; :: thesis: ex f being morphism of C st
( f1 |> f & f is right_identity )
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: ( f1 |> f & f is right_identity )
thus f1 |> f by A4; :: thesis: f is right_identity
thus f is right_identity by A4, Th18; :: thesis: verum

end;

hence C is with_right_identities ; :: thesis: verum