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