:: deftheorem defines iso ALTCAT_3:def 5 :
for C being category
for o1, o2 being Object of C
for A being Morphism of o1,o2 holds
( A is iso iff ( A * (A ") = idm o2 & (A ") * A = idm o1 ) );