theorem :: INSTALG1:30

for S1 being non empty ManySortedSign
for S2 being non empty Subsignature of S1
for A1, A2 being MSAlgebra over S1
for h being ManySortedFunction of the Sorts of A1, the Sorts of A2 holds h | the carrier of S2 is ManySortedFunction of the Sorts of (A1 | S2), the Sorts of (A2 | S2)