for S being non empty non void ManySortedSign
for U2, U3 being non-empty MSAlgebra over S
for F being ManySortedFunction of U2,U3 st F is_homomorphism U2,U3 holds
( F is_monomorphism U2,U3 iff for U1 being non-empty MSAlgebra over S
for h1, h2 being ManySortedFunction of U1,U2 st h1 is_homomorphism U1,U2 & h2 is_homomorphism U1,U2 & F ** h1 = F ** h2 holds
h1 = h2 )