:: deftheorem defines const PRALG_3:def 1 :
for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S holds const (o,U0) = (Den (o,U0)) . {};