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
(MSHomQuot F) ** (MSNat_Hom (A,(MSCng F))) = F