for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st the Sorts of A1 is_transformable_to the Sorts of A2 holds
for o being OperSymbol of S st Args (o,A1) <> {} holds
Args (o,A2) <> {}