:: deftheorem defines | INSTALG1:def 4 :
for S2, S1 being non empty ManySortedSign
for A being MSAlgebra over S2 holds A | S1 = A | (S1,(id the carrier of S1),(id the carrier' of S1));