theorem :: INSTALG1:28

for S1 being non empty feasible ManySortedSign
for S2 being non empty Subsignature of S1
for S3 being non empty Subsignature of S2
for A being MSAlgebra over S1 holds A | S3 = (A | S2) | S3