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_epimorphism U1,U2 & F is order-sorted holds
OSHomQuot F is_isomorphism QuotOSAlg (U1,(OSCng F)),U2