for S being non empty non void ManySortedSign
for U0, U1 being non-empty MSAlgebra over S
for W being strict non-empty free MSAlgebra over S
for F being ManySortedFunction of U0,U1 st F is_epimorphism U0,U1 holds
for G being ManySortedFunction of W,U1 st G is_homomorphism W,U1 holds
ex H being ManySortedFunction of W,U0 st
( H is_homomorphism W,U0 & G = F ** H )