( dom {} = {} & rng {} = {} )
;
then reconsider a = {} as Function of {},{} by FUNCT_2:1;
s is with_const_op
by Def3;
then consider o being OperSymbol of S such that
A1:
the Arity of S . o = {}
and
A2:
the ResultSort of S . o = s
by Def2;
A3:
dom the Arity of S = the carrier' of S
by FUNCT_2:def 1;
then
( dom ( the Sorts of U0 #) = the carrier of S * & the Arity of S . o in rng the Arity of S )
by FUNCT_1:def 3, PARTFUN1:def 2;
then A4:
o in dom (( the Sorts of U0 #) * the Arity of S)
by A3, FUNCT_1:11;
Args (o,U0) =
(( the Sorts of U0 #) * the Arity of S) . o
by MSUALG_1:def 4
.=
( the Sorts of U0 #) . ( the Arity of S . o)
by A4, FUNCT_1:12
.=
( the Sorts of U0 #) . (the_arity_of o)
by MSUALG_1:def 1
.=
product ( the Sorts of U0 * (the_arity_of o))
by FINSEQ_2:def 5
.=
product ( the Sorts of U0 * a)
by A1, MSUALG_1:def 1
.=
{{}}
by CARD_3:10
;
then A5:
{} in Args (o,U0)
by TARSKI:def 1;
set f = Den (o,U0);
A6:
rng (Den (o,U0)) c= Result (o,U0)
by RELAT_1:def 19;
dom (Den (o,U0)) = Args (o,U0)
by FUNCT_2:def 1;
then A7:
(Den (o,U0)) . {} in rng (Den (o,U0))
by A5, FUNCT_1:def 3;
A8:
dom the ResultSort of S = the carrier' of S
by FUNCT_2:def 1;
then
( dom the Sorts of U0 = the carrier of S & the ResultSort of S . o in rng the ResultSort of S )
by FUNCT_1:def 3, PARTFUN1:def 2;
then A9:
o in dom ( the Sorts of U0 * the ResultSort of S)
by A8, FUNCT_1:11;
Result (o,U0) =
( the Sorts of U0 * the ResultSort of S) . o
by MSUALG_1:def 5
.=
the Sorts of U0 . s
by A2, A9, FUNCT_1:12
;
then reconsider a = (Den (o,U0)) . {} as Element of the Sorts of U0 . s by A6, A7;
ex A being non empty set st
( A = the Sorts of U0 . s & Constants (U0,s) = { b where b is Element of A : ex o being OperSymbol of S st
( the Arity of S . o = {} & the ResultSort of S . o = s & b in rng (Den (o,U0)) ) } )
by Def4;
then
a in Constants (U0,s)
by A1, A2, A7;
hence
not Constants (U0,s) is empty
; verum