for S1, S2 being non empty ManySortedSign
for A being non-empty MSAlgebra over S2
for f, g being Function st f,g form_morphism_between S1,S2 holds
A | (S1,f,g) is non-empty