theorem Th4: :: PRALG_2:4

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 = {} holds
Args (o,U0) = {{}}