theorem :: INSTALG1:4

for S being non empty non void ManySortedSign
for A, B being MSAlgebra over S st MSAlgebra(# the Sorts of A, the Charact of A #) = MSAlgebra(# the Sorts of B, the Charact of B #) holds
for o being OperSymbol of S holds Den (o,A) = Den (o,B) ;