:: deftheorem defines monomorphism MOD_4:def 8 :
for K, L being non empty doubleLoopStr
for IT being Function of K,L holds
( IT is monomorphism iff ( IT is linear & IT is one-to-one ) );