for S1, S2 being non empty ManySortedSign
for f being Function of the carrier of S1, the carrier of S2
for g being Function st f,g form_morphism_between S1,S2 holds
for A1, A2 being MSAlgebra over S2
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h * f is ManySortedFunction of the Sorts of (A1 | (S1,f,g)), the Sorts of (A2 | (S1,f,g))