:: deftheorem defines with_units ALTCAT_2:def 9 :
for C being non empty AltCatStr holds
( C is with_units iff for o being Object of C holds
( <^o,o^> <> {} & ex i being Morphism of o,o st
for o9 being Object of C
for m9 being Morphism of o9,o
for m99 being Morphism of o,o9 holds
( ( <^o9,o^> <> {} implies i * m9 = m9 ) & ( <^o,o9^> <> {} implies m99 * i = m99 ) ) ) );