for S1 being non empty ManySortedSign
for S2 being non empty Subsignature of S1
for A being MSAlgebra over S1 holds (id the Sorts of A) | the carrier of S2 = id the Sorts of (A | S2)