( dom {} = {} & rng {} = {} )
;
then reconsider a = {} as Function of {} ,{} by FUNCT_2:3;
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 5, PARTFUN1:def 4;
then A4:
o in dom ((the Sorts of U0 # ) * the Arity of S)
by A3, FUNCT_1:21;
Args o,U0 =
((the Sorts of U0 # ) * the Arity of S) . o
by MSUALG_1:def 9
.=
(the Sorts of U0 # ) . (the Arity of S . o)
by A4, FUNCT_1:22
.=
(the Sorts of U0 # ) . (the_arity_of o)
by MSUALG_1:def 6
.=
product (the Sorts of U0 * (the_arity_of o))
by PBOOLE:def 19
.=
product (the Sorts of U0 * a)
by A1, MSUALG_1:def 6
.=
{{} }
by CARD_3:19
;
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 5;
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 5, PARTFUN1:def 4;
then A9:
o in dom (the Sorts of U0 * the ResultSort of S)
by A8, FUNCT_1:21;
Result o,U0 =
(the Sorts of U0 * the ResultSort of S) . o
by MSUALG_1:def 10
.=
the Sorts of U0 . s
by A2, A9, FUNCT_1:22
;
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