let S be non empty non void ManySortedSign ; :: thesis: 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)
let U0 be MSAlgebra over S; :: thesis: for o being OperSymbol of S st the_arity_of o = {} & Result (o,U0) <> {} holds
const (o,U0) in Result (o,U0)
let o be OperSymbol of S; :: thesis: ( the_arity_of o = {} & Result (o,U0) <> {} implies const (o,U0) in Result (o,U0) )
assume that
A1: the_arity_of o = {} and
A2: Result (o,U0) <> {} ; :: thesis: const (o,U0) in Result (o,U0)
dom (Den (o,U0)) = Args (o,U0) by A2, FUNCT_2:def 1
.= {{}} by A1, PRALG_2:4 ;
then {} in dom (Den (o,U0)) by TARSKI:def 1;
then (Den (o,U0)) . {} in rng (Den (o,U0)) by FUNCT_1:def 3;
hence const (o,U0) in Result (o,U0) ; :: thesis: verum