for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for A being MSSubAlgebra of U0
for o being OperSymbol of S
for x being set st x in Args (o,A) holds
(Den (o,A)) . x = (Den (o,U0)) . x