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

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

assume A1: C is with_left_identities ; :: thesis: CategoryStr(# the carrier of C, the composition of C #) is with_left_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
( g |> g1 & g is left_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
( g |> g1 & g is left_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
( g |> g1 & g is left_identity )
then consider f being morphism of C such that
A2: ( f |> f1 & f is left_identity ) by A1;
reconsider g = f as morphism of CategoryStr(# the carrier of C, the composition of C #) ;
take g ; :: thesis: ( g |> g1 & g is left_identity )
thus g |> g1 by A2; :: thesis: g is left_identity
thus g is left_identity by A2, Th16; :: thesis: verum

end;

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

end;

assume A3: CategoryStr(# the carrier of C, the composition of C #) is with_left_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 ) )
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
( f |> f1 & f is left_identity )
then consider g being morphism of CategoryStr(# the carrier of C, the composition of C #) such that
A4: ( g |> g1 & g is left_identity ) by A3;
reconsider f = g as morphism of C ;
take f ; :: thesis: ( f |> f1 & f is left_identity )
thus f |> f1 by A4; :: thesis: f is left_identity
thus f is left_identity by A4, Th16; :: thesis: verum

end;

hence C is with_left_identities ; :: thesis: verum