theorem :: OSALG_4:25

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