:: deftheorem Def6 defines with_left_identities CAT_6:def 6 :
for C being CategoryStr holds
( C is with_left_identities iff 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 ) );