theorem :: MSUALG_9:36

for S being non empty non void ManySortedSign
for A, B being non-empty MSAlgebra over S
for F being ManySortedFunction of A,B st F is_homomorphism A,B holds
for C1 being MSCongruence of A st C1 c= MSCng F holds
ex H being ManySortedFunction of (QuotMSAlg (A,C1)),B st
( H is_homomorphism QuotMSAlg (A,C1),B & F = H ** (MSNat_Hom (A,C1)) )