( dom {} = {} & rng {} = {} )
;

then reconsider a = {} as Function of {},{} by FUNCT_2:1;

s is with_const_op by Def2;

then consider o being OperSymbol of S such that

A1: the Arity of S . o = {} and

A2: the ResultSort of S . o = s ;

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 Def3;

then a in Constants (U0,s) by A1, A2, A7;

hence not Constants (U0,s) is empty ; :: thesis: verum

then reconsider a = {} as Function of {},{} by FUNCT_2:1;

s is with_const_op by Def2;

then consider o being OperSymbol of S such that

A1: the Arity of S . o = {} and

A2: the ResultSort of S . o = s ;

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 Def3;

then a in Constants (U0,s) by A1, A2, A7;

hence not Constants (U0,s) is empty ; :: thesis: verum