:: deftheorem defines identity CAT_6:def 14 :
for C being CategoryStr
for f being morphism of C holds
( f is identity iff ( f is left_identity & f is right_identity ) );