:: deftheorem Def4 defines left_identity CAT_6:def 4 :
for C being CategoryStr
for f being morphism of C holds
( f is left_identity iff for f1 being morphism of C st f |> f1 holds
f (*) f1 = f1 );