let S be non empty non void ManySortedSign ; :: thesis: for U0 being MSAlgebra of 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 of 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:11 ;
then {} in dom (Den o,U0) by TARSKI:def 1;
then (Den o,U0) . {} in rng (Den o,U0) by FUNCT_1:def 5;
hence const o,U0 in Result o,U0 ; :: thesis: verum