:: deftheorem defines is_monomorphism MSUALG_3:def 9 :
for S being non empty non void ManySortedSign
for U1, U2 being MSAlgebra over S
for F being ManySortedFunction of U1,U2 holds
( F is_monomorphism U1,U2 iff ( F is_homomorphism U1,U2 & F is "1-1" ) );