for S being locally_directed OrderSortedSign
for U1, U2 being non-empty OSAlgebra of S
for F being ManySortedFunction of U1,U2 st F is_homomorphism U1,U2 & F is order-sorted holds
( OSHomQuot F is_monomorphism QuotOSAlg (U1,(OSCng F)),U2 & OSHomQuot F is order-sorted )