for S1, S2 being non empty ManySortedSign
for f, g being Function st f,g form_morphism_between S1,S2 holds
for A being MSAlgebra over S2 holds (id the Sorts of A) * f = id the Sorts of (A | (S1,f,g))