s is with_const_op by Def3;
then consider o being OperSymbol of S such that
A1: ( the Arity of S . o = {} & the ResultSort of S . o = s ) by Def2;
A3: dom (the Sorts of U0 # ) = the carrier of S * by PBOOLE:def 3;
A4: ( dom the Arity of S = the carrier' of S & rng the Arity of S c= the carrier of S * ) by FUNCT_2:def 1, RELSET_1:12;
then the Arity of S . o in rng the Arity of S by FUNCT_1:def 5;
then A5: o in dom ((the Sorts of U0 # ) * the Arity of S) by A3, A4, FUNCT_1:21;
set f = Den o,U0;
( dom {} = {} & rng {} = {} ) ;
then reconsider a = {} as Function of {} , {} by FUNCT_2:3;
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 A5, 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 A6: {} in Args o,U0 by TARSKI:def 1;
A7: ( dom (Den o,U0) = Args o,U0 & rng (Den o,U0) c= Result o,U0 ) by FUNCT_2:def 1, RELSET_1:12;
then A8: (Den o,U0) . {} in rng (Den o,U0) by A6, FUNCT_1:def 5;
A9: dom the Sorts of U0 = the carrier of S by PBOOLE:def 3;
A10: ( dom the ResultSort of S = the carrier' of S & rng the ResultSort of S c= the carrier of S ) by FUNCT_2:def 1, RELSET_1:12;
then the ResultSort of S . o in rng the ResultSort of S by FUNCT_1:def 5;
then A11: o in dom (the Sorts of U0 * the ResultSort of S) by A9, A10, 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 A1, A11, FUNCT_1:22 ;
then reconsider a = (Den o,U0) . {} as Element of the Sorts of U0 . s by A7, A8;
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, A8;
hence not Constants U0,s is empty ; :: thesis: verum