theorem Th27: :: CIRCCOMB:27

for S1, S2 being non empty non void ManySortedSign
for A1 being non-empty MSAlgebra over S1
for A2 being non-empty MSAlgebra over S2 st the Sorts of A1 tolerates the Sorts of A2 holds
for o being OperSymbol of (S1 +* S2)
for o2 being OperSymbol of S2 st o = o2 holds
Den (o,(A1 +* A2)) = Den (o2,A2)