reconsider St = the Sorts of U1 as V2() ManySortedSet of the carrier of S ;
consider s being SortSymbol of S;
dom the Sorts of U1 = the carrier of S by PARTFUN1:def 4;
then A1: the Sorts of U1 . s in rng the Sorts of U1 by FUNCT_1:def 5;
ex x being set st x in St . s by XBOOLE_0:def 1;
hence not |.U1.| is empty by A1, TARSKI:def 4; :: thesis: verum