theorem Th24: :: MSAFREE4:24

for S being non empty non void ManySortedSign
for A1, A2 being MSAlgebra over S st MSAlgebra(# the Sorts of A1, the Charact of A1 #) = MSAlgebra(# the Sorts of A2, the Charact of A2 #) holds
for B1 being MSSubset of A1
for B2 being MSSubset of A2 st B1 = B2 holds
for o being OperSymbol of S st B1 is_closed_on o holds
B2 is_closed_on o ;