for S being non empty non void ManySortedSign
for U0 being non-empty MSAlgebra over S
for A being feasible MSAlgebra over S
for C being feasible MSSubAlgebra of A
for D being ManySortedSubset of the Sorts of A st D = the Sorts of C holds
for h being ManySortedFunction of A,U0 st h is_homomorphism A,U0 holds
for g being ManySortedFunction of C,U0 st g = h || D holds
g is_homomorphism C,U0