theorem Th5: :: PRALG_3:5

for S being non empty non void ManySortedSign
for U0 being MSAlgebra over S
for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds
const (o,U0) in Result (o,U0)