( 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 ;
then A4: o in dom (( the Sorts of U0 #) * the Arity of S) by ;
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
.= ( the Sorts of U0 #) . () by MSUALG_1:def 1
.= product ( the Sorts of U0 * ()) by FINSEQ_2:def 5
.= product ( the Sorts of U0 * a) by
.= 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 ;
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 ;
then A9: o in dom ( the Sorts of U0 * the ResultSort of S) by ;
Result (o,U0) = ( the Sorts of U0 * the ResultSort of S) . o by MSUALG_1:def 5
.= the Sorts of U0 . s by ;
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