theorem :: MSUALG_4:3

for S being non empty non void ManySortedSign
for U1 being non-empty MSAlgebra over S
for R being MSCongruence of U1 holds MSNat_Hom (U1,R) is_epimorphism U1, QuotMSAlg (U1,R)