for S being non void feasible ManySortedSign
for S9 being non void Subsignature of S
for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for h being ManySortedFunction of A1,A2 st h is_homomorphism A1,A2 holds
ex h9 being ManySortedFunction of (A1 | S9),(A2 | S9) st
( h9 = h | the carrier of S9 & h9 is_homomorphism A1 | S9,A2 | S9 )